| 03d3eb0 | SimonBoulier | 11 September 2019, 16:34:42 UTC | A few conv lemmas in SafeLemmata | 12 September 2019, 09:23:40 UTC |
| 486ff2e | Théo Winterhalter | 12 September 2019, 08:36:37 UTC | Merge pull request #269 from MetaCoq/alpha-case Add sorting information on branches of pattern-matching | 12 September 2019, 08:36:37 UTC |
| bc4bd9b | Théo Winterhalter | 11 September 2019, 17:21:06 UTC | Complete typing_alpha Yay! | 11 September 2019, 17:23:44 UTC |
| b634781 | Théo Winterhalter | 11 September 2019, 14:51:45 UTC | Add sorting information on branches of pattern-matching Warning: Adds an admit in SafeChecker | 11 September 2019, 16:12:52 UTC |
| 4c779c7 | Théo Winterhalter | 11 September 2019, 11:50:51 UTC | Merge pull request #263 from MetaCoq/nameless Progress with α-renaming (eq_term) | 11 September 2019, 11:50:51 UTC |
| 12635ba | Théo Winterhalter | 11 September 2019, 11:24:33 UTC | Merge remote-tracking branch 'Template-Coq/coq-8.8' into nameless | 11 September 2019, 11:24:33 UTC |
| 1735844 | Théo Winterhalter | 11 September 2019, 10:28:44 UTC | CoFix case of typing_alpha | 11 September 2019, 10:28:44 UTC |
| ca76c74 | SimonBoulier | 11 September 2019, 09:56:31 UTC | Fix comparison of instances in eq_term_upto_univ + admit in Confluence | 11 September 2019, 10:26:54 UTC |
| 0857d7e | SimonBoulier | 11 September 2019, 09:56:19 UTC | Remove unused lemma | 11 September 2019, 10:26:54 UTC |
| fcac06f | SimonBoulier | 11 September 2019, 09:16:19 UTC | Remove unused red_nl | 11 September 2019, 10:26:54 UTC |
| 5e16f6e | SimonBoulier | 10 September 2019, 13:19:46 UTC | One admit in SigmaCalculus | 11 September 2019, 10:26:54 UTC |
| ad5aa7b | Théo Winterhalter | 11 September 2019, 09:41:36 UTC | Rename type_rename into typing_alpha | 11 September 2019, 09:41:36 UTC |
| 749bd96 | Théo Winterhalter | 11 September 2019, 09:28:42 UTC | Complete tFix case of type_rename | 11 September 2019, 09:28:42 UTC |
| ca03206 | Théo Winterhalter | 10 September 2019, 13:53:29 UTC | Attempt at extracting sorting information from wf_local of fix_context | 10 September 2019, 13:53:29 UTC |
| b0b1601 | SimonBoulier | 04 September 2019, 10:57:27 UTC | UnivSubst! | 10 September 2019, 13:18:43 UTC |
| aeb620d | SimonBoulier | 27 August 2019, 11:18:59 UTC | Two minor admits in TemplateToPCUIC | 10 September 2019, 13:18:43 UTC |
| cf52429 | Théo Winterhalter | 10 September 2019, 12:28:35 UTC | Style | 10 September 2019, 12:28:35 UTC |
| 48028c5 | Théo Winterhalter | 10 September 2019, 12:00:14 UTC | Refactor a bit in type_rename proof to avoid duplication | 10 September 2019, 12:00:14 UTC |
| d8a77c3 | Théo Winterhalter | 10 September 2019, 11:50:14 UTC | Almost done with type_rename/tFix | 10 September 2019, 11:50:14 UTC |
| f62f83f | Théo Winterhalter | 10 September 2019, 11:21:38 UTC | Prove eq_context_upto_conv_context and progress with tFix (type_rename) | 10 September 2019, 11:21:53 UTC |
| a302cbc | Matthieu Sozeau | 10 September 2019, 10:11:35 UTC | Merge pull request #266 from MetaCoq/fixup-univs Fix erasure calling typing on a well-formed arity which might not be a | 10 September 2019, 10:11:35 UTC |
| 2497669 | Théo Winterhalter | 10 September 2019, 08:35:27 UTC | Use proper context conversion | 10 September 2019, 08:35:27 UTC |
| 11f82cc | Matthieu Sozeau | 10 September 2019, 07:22:08 UTC | Fix erasure calling typing on a well-formed arity which might not be a type (e.g. lists's type ends in an algebraic) | 10 September 2019, 07:22:08 UTC |
| 4c92247 | Matthieu Sozeau | 10 September 2019, 07:02:58 UTC | Merge pull request #264 from MetaCoq/fixup-univs Fixup univs | 10 September 2019, 07:02:58 UTC |
| 8823a67 | Matthieu Sozeau | 09 September 2019, 15:19:21 UTC | Actually, fold left to right | 09 September 2019, 15:19:35 UTC |
| a6948c8 | Théo Winterhalter | 09 September 2019, 15:06:56 UTC | Some progress with type_rename for eq_term | 09 September 2019, 15:06:56 UTC |
| 500fbe5 | Théo Winterhalter | 09 September 2019, 13:21:48 UTC | Clean PCUICNameless module | 09 September 2019, 14:28:28 UTC |
| a79cb91 | Matthieu Sozeau | 09 September 2019, 13:21:11 UTC | Update .gitignore | 09 September 2019, 13:21:38 UTC |
| 9a9146d | Matthieu Sozeau | 09 September 2019, 13:10:47 UTC | Deactivate PCUIC plugin installation: another extraction issue | 09 September 2019, 13:21:38 UTC |
| 8710798 | Matthieu Sozeau | 09 September 2019, 12:39:20 UTC | Fix clean_extraction.sh script and Makefile (name clash of deps files) | 09 September 2019, 13:21:38 UTC |
| 9d04769 | Matthieu Sozeau | 09 September 2019, 13:11:39 UTC | Merge pull request #262 from MetaCoq/fixup-univs Fixup univs | 09 September 2019, 13:11:39 UTC |
| 1db2641 | Matthieu Sozeau | 09 September 2019, 11:58:19 UTC | fold right instead | 09 September 2019, 11:58:19 UTC |
| f5fa34b | Matthieu Sozeau | 09 September 2019, 10:18:39 UTC | Add a function to fixup universe declarations in the global environment, now used in the safe checker and safe erasure | 09 September 2019, 10:20:01 UTC |
| 8fe6ff2 | Matthieu Sozeau | 06 September 2019, 15:26:20 UTC | Merge pull request #258 from MetaCoq/safelemmata_cleaning Small cleaning in SafeLemmata | 06 September 2019, 15:26:20 UTC |
| e0940c1 | Matthieu Sozeau | 06 September 2019, 15:25:17 UTC | Merge pull request #261 from MetaCoq/sigma-renaming Renaming in the σ-calculus (modulo pattern-matching) | 06 September 2019, 15:25:17 UTC |
| e26597c | Théo Winterhalter | 06 September 2019, 14:57:28 UTC | Complete cumul case of type_rename | 06 September 2019, 14:57:28 UTC |
| 05f8113 | Théo Winterhalter | 06 September 2019, 14:45:17 UTC | Prove tCoFix case of type_rename | 06 September 2019, 14:45:17 UTC |
| 45cbeb2 | Théo Winterhalter | 06 September 2019, 14:40:23 UTC | Complete tFix case of type_rename | 06 September 2019, 14:40:23 UTC |
| dfe5246 | Théo Winterhalter | 06 September 2019, 14:37:41 UTC | Deal properly with wf_local for tFix (type_rename) | 06 September 2019, 14:37:41 UTC |
| 95525f3 | Matthieu Sozeau | 06 September 2019, 14:06:55 UTC | Merge pull request #260 from MetaCoq/fix-pcuic-plugin-compile Build PCUIC plugin again, needed by CertiCoq | 06 September 2019, 14:06:55 UTC |
| 05185f4 | Théo Winterhalter | 06 September 2019, 14:05:08 UTC | Deal with fix modulo `wf_local` of new `fix_context` | 06 September 2019, 14:05:08 UTC |
| 329b57b | Matthieu Sozeau | 06 September 2019, 13:46:18 UTC | Build PCUIC plugin again, needed by CertiCoq | 06 September 2019, 13:46:18 UTC |
| c65a4a0 | Théo Winterhalter | 06 September 2019, 13:09:41 UTC | Prove forall_nth_error_All Also clean ugly proof of `forall_nth_error_Alli`. | 06 September 2019, 13:09:41 UTC |
| 232964f | Théo Winterhalter | 06 September 2019, 13:03:52 UTC | Progress with tFix for type_rename | 06 September 2019, 13:03:52 UTC |
| 51fda38 | Théo Winterhalter | 06 September 2019, 12:44:22 UTC | Merge pull request #259 from MetaCoq/sigma-renaming Fix bug that somehow passed CI | 06 September 2019, 12:44:22 UTC |
| 67cb604 | Théo Winterhalter | 06 September 2019, 12:00:28 UTC | Update gitignore | 06 September 2019, 12:00:28 UTC |
| 1dceff2 | Théo Winterhalter | 06 September 2019, 11:58:50 UTC | Add PCUICSigmaCalculus to CoqProject | 06 September 2019, 11:58:50 UTC |
| bf340ed | Théo Winterhalter | 06 September 2019, 11:42:27 UTC | Fix bug that somehow passed CI | 06 September 2019, 11:42:27 UTC |
| 6de6b2c | Théo Winterhalter | 06 September 2019, 09:45:41 UTC | Merge pull request #256 from MetaCoq/sigma-renaming More σ-calculus (especially renaming) | 06 September 2019, 09:45:41 UTC |
| 08c0363 | Théo Winterhalter | 06 September 2019, 09:19:29 UTC | Minor remark change | 06 September 2019, 09:19:29 UTC |
| 12fedea | SimonBoulier | 05 September 2019, 16:10:05 UTC | Small cleaning in SafeLemmata | 05 September 2019, 16:10:05 UTC |
| c616c1f | Théo Winterhalter | 05 September 2019, 13:44:01 UTC | Clean away some lemmata from σ-calculus module | 05 September 2019, 14:18:53 UTC |
| 4269e96 | Matthieu Sozeau | 05 September 2019, 07:29:49 UTC | Merge pull request #254 from MetaCoq/pretty-print-univ-error Better pretty-printing of universe error | 05 September 2019, 07:29:49 UTC |
| 3a1fb40 | Théo Winterhalter | 04 September 2019, 13:00:40 UTC | Deal with cumul case in typing_rename | 04 September 2019, 13:00:40 UTC |
| 87e4849 | Théo Winterhalter | 04 September 2019, 12:56:37 UTC | Prove cumul_refl | 04 September 2019, 12:56:37 UTC |
| c1937cf | Théo Winterhalter | 04 September 2019, 12:55:16 UTC | Almost prove cumul_rename | 04 September 2019, 12:55:16 UTC |
| 479af89 | Théo Winterhalter | 04 September 2019, 12:42:04 UTC | Complete red1_rename | 04 September 2019, 12:42:04 UTC |
| 623e8f6 | Théo Winterhalter | 04 September 2019, 12:21:20 UTC | Somehow proved supposedly wrong statement of rename_fix_context | 04 September 2019, 12:21:20 UTC |
| 1f2cceb | Théo Winterhalter | 04 September 2019, 11:37:42 UTC | Prove urenaming_context | 04 September 2019, 11:37:42 UTC |
| 04d97ce | Théo Winterhalter | 04 September 2019, 11:20:33 UTC | Prove extensionality of urenaming | 04 September 2019, 11:20:33 UTC |
| b1dd640 | Théo Winterhalter | 04 September 2019, 09:17:10 UTC | Use OnOne2_ind_l to progress with fix case in red1_rename | 04 September 2019, 09:17:10 UTC |
| 486fe2d | Théo Winterhalter | 03 September 2019, 14:54:22 UTC | Deal with all cases for red1_rename except (co)fix hard two cases | 03 September 2019, 14:54:22 UTC |
| a3ecc97 | Théo Winterhalter | 03 September 2019, 14:37:52 UTC | Deal with most cases of red1_rename | 03 September 2019, 14:37:52 UTC |
| b72ae25 | Théo Winterhalter | 03 September 2019, 14:13:47 UTC | Better definition of renaming | 03 September 2019, 14:13:47 UTC |
| 36ee957 | Théo Winterhalter | 03 September 2019, 14:08:34 UTC | Weaker notion of valid renaming | 03 September 2019, 14:08:34 UTC |
| d91319d | Théo Winterhalter | 03 September 2019, 14:04:51 UTC | red1_rename should not be about full renaming predicate | 03 September 2019, 14:04:51 UTC |
| eea31a3 | Théo Winterhalter | 03 September 2019, 13:58:53 UTC | Complete red_proj case | 03 September 2019, 13:58:53 UTC |
| ea95d65 | Théo Winterhalter | 03 September 2019, 13:31:43 UTC | Prove declared_constant_closed_body | 03 September 2019, 13:31:43 UTC |
| 88e19c4 | Théo Winterhalter | 03 September 2019, 13:19:23 UTC | Prove rename_unfold_cofix | 03 September 2019, 13:19:23 UTC |
| 523a45a | Théo Winterhalter | 03 September 2019, 13:08:20 UTC | Multiple lemma to deal with fix unfolding in red1_rename | 03 September 2019, 13:08:20 UTC |
| efe14cd | Théo Winterhalter | 03 September 2019, 12:18:37 UTC | Prove rename_iota_red | 03 September 2019, 12:18:37 UTC |
| 22fd0bb | Théo Winterhalter | 03 September 2019, 11:47:25 UTC | Merge pull request #255 from MetaCoq/compile-fix Fix sed invocations for macOS | 03 September 2019, 11:47:25 UTC |
| b889876 | Théo Winterhalter | 03 September 2019, 11:46:26 UTC | Fix red1_rename statement | 03 September 2019, 11:46:26 UTC |
| 8bc774c | Théo Winterhalter | 02 September 2019, 13:46:27 UTC | Fix sed invocations for macOS | 02 September 2019, 13:46:27 UTC |
| c6ee3e7 | Matthieu Sozeau | 26 August 2019, 10:10:15 UTC | Better pretty-printing of universe error | 26 August 2019, 14:43:58 UTC |
| 26cc211 | Matthieu Sozeau | 26 August 2019, 10:14:03 UTC | Merge pull request #253 from MetaCoq/clean_pcuic_equality Big clean of PCUICEquality.v and remove useless axioms | 26 August 2019, 10:14:03 UTC |
| 455b40f | SimonBoulier | 26 August 2019, 09:44:18 UTC | comment plgin target | 26 August 2019, 09:44:18 UTC |
| f3b8bbe | SimonBoulier | 23 August 2019, 16:08:04 UTC | Remove useless axioms | 26 August 2019, 09:23:04 UTC |
| 4abda76 | SimonBoulier | 23 August 2019, 14:36:02 UTC | Big clean of PCUICEquality.v | 26 August 2019, 09:23:04 UTC |
| bd97783 | Matthieu Sozeau | 22 August 2019, 15:23:12 UTC | Forgot one file to patch... | 22 August 2019, 15:29:48 UTC |
| f32f814 | Matthieu Sozeau | 22 August 2019, 15:12:16 UTC | Merge pull request #251 from MetaCoq/fix-equations-set-keyed-unif Explicitely [Set Keyed Unification] which was implicitely exported by | 22 August 2019, 15:12:16 UTC |
| bec2c23 | Matthieu Sozeau | 22 August 2019, 14:55:27 UTC | Explicitely [Set Keyed Unification] which was implicitely exported by Equations (backwards compat with equations-1.2) | 22 August 2019, 14:55:27 UTC |
| 4308702 | Matthieu Sozeau | 22 August 2019, 13:03:10 UTC | Merge pull request #250 from MetaCoq/extract-eliftsubst Extract ELiftSubst and ETyping needed by certicoq | 22 August 2019, 13:03:10 UTC |
| 11f4741 | Matthieu Sozeau | 22 August 2019, 13:02:17 UTC | Merge pull request #249 from MetaCoq/parameterize-checker-flags Make things more parametric on checker_flags | 22 August 2019, 13:02:17 UTC |
| 012145e | Matthieu Sozeau | 22 August 2019, 12:11:48 UTC | Extract ELiftSubst and ETyping needed by certicoq | 22 August 2019, 12:12:16 UTC |
| 2dbbe3c | Matthieu Sozeau | 22 August 2019, 09:20:42 UTC | Merge pull request #248 from MetaCoq/safechecker2 Lemmas for safechecker | 22 August 2019, 09:20:42 UTC |
| 68ad79c | SimonBoulier | 22 August 2019, 07:09:44 UTC | Typing of nameless | 22 August 2019, 07:09:44 UTC |
| 25baf91 | Matthieu Sozeau | 20 August 2019, 16:46:31 UTC | Make things more parametric on checker_flags | 20 August 2019, 16:46:31 UTC |
| 0f04fc3 | SimonBoulier | 20 August 2019, 07:41:14 UTC | Universes taken in account in conversion checking + more on checking of globenvs | 20 August 2019, 07:41:14 UTC |
| 9808153 | SimonBoulier | 19 August 2019, 10:43:12 UTC | fix compil | 19 August 2019, 10:43:12 UTC |
| 2309c28 | SimonBoulier | 19 August 2019, 10:17:47 UTC | Prove admitted lemmas in WeakeningEnv | 19 August 2019, 10:39:23 UTC |
| e2fbd86 | SimonBoulier | 19 August 2019, 08:33:29 UTC | Renaming in uGraph | 19 August 2019, 10:39:23 UTC |
| e1bcfcc | SimonBoulier | 16 August 2019, 17:07:07 UTC | Remove duplicate | 19 August 2019, 10:39:23 UTC |
| 0d295ee | SimonBoulier | 16 August 2019, 16:21:29 UTC | Transitivity of string comparison | 16 August 2019, 16:48:08 UTC |
| 7bcd478 | Matthieu Sozeau | 15 August 2019, 19:08:16 UTC | Merge pull request #245 from MetaCoq/ewcbveval-evalfix Fix EWcbvEval fix evaluation rule, spotted by R. Pollack | 15 August 2019, 19:08:16 UTC |
| 0abd687 | Matthieu Sozeau | 15 August 2019, 18:35:31 UTC | Fix EWcbvEval fix evaluation rule, spotted by R. Pollack | 15 August 2019, 18:35:42 UTC |
| 27cc3e4 | Matthieu Sozeau | 06 August 2019, 19:28:40 UTC | Merge pull request #244 from MetaCoq/fix-install-targets Fix install targets | 06 August 2019, 19:28:40 UTC |
| 9f716fe | Matthieu Sozeau | 06 August 2019, 16:34:41 UTC | Fix install targets | 06 August 2019, 16:38:26 UTC |
| 348fc4e | Matthieu Sozeau | 30 July 2019, 04:29:27 UTC | Merge pull request #243 from MetaCoq/wcbveval-template WcbvEval | 30 July 2019, 04:29:27 UTC |
| 91a56eb | Matthieu Sozeau | 30 July 2019, 04:01:51 UTC | Progress on wcbvEval determinism | 30 July 2019, 04:01:51 UTC |
