| 1f19520 | Théo Winterhalter | 19 September 2019, 20:28:45 UTC | Change checker printing a bit for clarity | 19 September 2019, 20:46:31 UTC |
| d972f5c | Théo Winterhalter | 19 September 2019, 20:13:56 UTC | Add one more fallback just in case | 19 September 2019, 20:13:56 UTC |
| 238c7d7 | Théo Winterhalter | 19 September 2019, 20:02:49 UTC | Fix conversion after putting context conversion as hyp | 19 September 2019, 20:02:49 UTC |
| 0d41cf6 | Théo Winterhalter | 19 September 2019, 18:12:22 UTC | [WIP] Require conv_ctx_stack instead of proving it | 19 September 2019, 18:12:22 UTC |
| 4c53d82 | Théo Winterhalter | 19 September 2019, 16:32:28 UTC | Dealing with incompleteness a bit | 19 September 2019, 16:32:28 UTC |
| 34acd83 | Théo Winterhalter | 19 September 2019, 15:09:37 UTC | Only compare stacks with Conv and not Cumul, using nleq_term first | 19 September 2019, 15:09:37 UTC |
| 7e8f9ec | Théo Winterhalter | 19 September 2019, 14:10:35 UTC | Add missing case on conversion fallback There is a slight problem with the obligations that are generated though... | 19 September 2019, 14:10:35 UTC |
| 94cd659 | SimonBoulier | 19 September 2019, 09:39:43 UTC | leb kelim instead of eq for type_Case | 19 September 2019, 10:11:38 UTC |
| c938e00 | Théo Winterhalter | 18 September 2019, 20:02:08 UTC | Merge pull request #283 from MetaCoq/reduce-stack-rollback Rollback old version of reduce_stack_full (axiom free) | 18 September 2019, 20:02:08 UTC |
| 119476a | Théo Winterhalter | 18 September 2019, 19:28:47 UTC | Rollback old version of reduce_stack_full (axiom free) | 18 September 2019, 19:28:47 UTC |
| 748f969 | Théo Winterhalter | 18 September 2019, 17:02:57 UTC | Merge pull request #282 from MetaCoq/remove-red-ctx-conv Remove red_context_conversion (false) axiom | 18 September 2019, 17:02:57 UTC |
| 8b37013 | Théo Winterhalter | 18 September 2019, 16:01:38 UTC | Move conv_context_convp in Safe Lemmata | 18 September 2019, 16:01:38 UTC |
| 1aafc8a | Théo Winterhalter | 18 September 2019, 15:50:57 UTC | Remove false axiom red_context_conversion | 18 September 2019, 15:50:57 UTC |
| 9ce5ccd | Théo Winterhalter | 18 September 2019, 13:23:31 UTC | Merge pull request #281 from MetaCoq/minor Minor changes (gitignore + comment about error message) | 18 September 2019, 13:23:31 UTC |
| 53e803e | Théo Winterhalter | 18 September 2019, 12:44:50 UTC | Update gitignore | 18 September 2019, 12:44:50 UTC |
| 6ca16df | Théo Winterhalter | 18 September 2019, 12:44:24 UTC | Update error when checking checker | 18 September 2019, 12:44:24 UTC |
| a4e2ca6 | Théo Winterhalter | 17 September 2019, 17:52:14 UTC | Merge pull request #280 from MetaCoq/clean-conversion Clean conversion | 17 September 2019, 17:52:14 UTC |
| e451cf4 | Théo Winterhalter | 17 September 2019, 15:21:03 UTC | Merge remote-tracking branch 'Template-Coq/coq-8.8' into clean-conversion | 17 September 2019, 15:21:03 UTC |
| 4ee4894 | Théo Winterhalter | 17 September 2019, 15:17:59 UTC | Remove TODOs for now | 17 September 2019, 15:17:59 UTC |
| ce54982 | Théo Winterhalter | 17 September 2019, 14:56:18 UTC | Move some zipc lemmata | 17 September 2019, 15:10:06 UTC |
| 9ae5cd4 | Théo Winterhalter | 17 September 2019, 14:42:11 UTC | Move red_context_conversion to ContextConversion module | 17 September 2019, 14:42:11 UTC |
| 9188560 | Théo Winterhalter | 17 September 2019, 13:14:53 UTC | Move cored utility to PCUICSN | 17 September 2019, 13:53:57 UTC |
| dbf4fbc | Matthieu Sozeau | 17 September 2019, 13:48:56 UTC | Merge pull request #278 from MetaCoq/safelemmas2 wf_local_red and other lemmas | 17 September 2019, 13:48:56 UTC |
| 64d8941 | Théo Winterhalter | 17 September 2019, 13:43:25 UTC | Merge pull request #279 from MetaCoq/cored-upto Towards reasoning on reduction modulo names | 17 September 2019, 13:43:25 UTC |
| 97224c5 | Théo Winterhalter | 17 September 2019, 12:35:48 UTC | Remove nlpack as it was a duplicate of pack | 17 September 2019, 12:35:48 UTC |
| 8b354c9 | Théo Winterhalter | 17 September 2019, 12:03:36 UTC | Use cored' instead of cored This includes the proof of many auxiliary lemmata. | 17 September 2019, 12:24:06 UTC |
| cb47f44 | SimonBoulier | 17 September 2019, 10:00:10 UTC | remove now useless axiom | 17 September 2019, 12:13:32 UTC |
| 3817a32 | Théo Winterhalter | 17 September 2019, 09:40:41 UTC | Prove normalisation_upto | 17 September 2019, 09:40:41 UTC |
| eda46f9 | Théo Winterhalter | 17 September 2019, 09:38:46 UTC | Prove Acc_cored_cored' | 17 September 2019, 09:38:46 UTC |
| 386c62b | SimonBoulier | 17 September 2019, 09:34:28 UTC | wf_local_red and other lemmas | 17 September 2019, 09:37:46 UTC |
| aa971e4 | Matthieu Sozeau | 17 September 2019, 07:48:33 UTC | Merge pull request #277 from lgaeher/coq-8.8 fix configure.sh, add hint about configure.sh to installation instructions | 17 September 2019, 07:48:33 UTC |
| 94b1fdd | Lennard Gäher | 17 September 2019, 07:20:29 UTC | fix configure.sh, add hint about configure.sh to installation instructions | 17 September 2019, 07:20:29 UTC |
| 50a3034 | Théo Winterhalter | 16 September 2019, 17:57:34 UTC | Prove cored_upto | 16 September 2019, 17:57:34 UTC |
| 71d060e | Théo Winterhalter | 16 September 2019, 17:23:16 UTC | Progress with normalisation_upto | 16 September 2019, 17:23:16 UTC |
| e818b57 | Théo Winterhalter | 16 September 2019, 17:02:52 UTC | Prove Acc_impl | 16 September 2019, 17:02:52 UTC |
| 297be9b | Théo Winterhalter | 16 September 2019, 15:28:58 UTC | Some properties on cored with hope of fixing cored_nl eventually | 16 September 2019, 15:28:58 UTC |
| ccf1674 | Théo Winterhalter | 16 September 2019, 12:08:37 UTC | Merge pull request #276 from MetaCoq/pcuic-alpha wellformed_alpha + wellformed_nlctx + a bit of cleaning (PCUICAlpha) | 16 September 2019, 12:08:37 UTC |
| a655d56 | SimonBoulier | 16 September 2019, 11:43:08 UTC | wellformed_nlctx | 16 September 2019, 11:43:08 UTC |
| 41161ad | SimonBoulier | 16 September 2019, 11:19:11 UTC | wellformed_alpha + a bit of cleaning | 16 September 2019, 11:19:11 UTC |
| 3ebc604 | SimonBoulier | 16 September 2019, 09:45:11 UTC | New file PCUICAlpha | 16 September 2019, 09:45:11 UTC |
| 14d85c6 | Matthieu Sozeau | 15 September 2019, 16:44:11 UTC | Merge pull request #267 from MetaCoq/erasure-retyping-switch Erasure retyping switch | 15 September 2019, 16:44:11 UTC |
| 31748a1 | Matthieu Sozeau | 15 September 2019, 16:22:24 UTC | Make SafeTemplateErasure's assume_wf_decl hack transparent so that things can compute more inside Coq | 15 September 2019, 16:22:24 UTC |
| f1c6d44 | Matthieu Sozeau | 15 September 2019, 14:49:45 UTC | Merge pull request #274 from MetaCoq/remove-zipx Remove zipx from safe conversion | 15 September 2019, 14:49:45 UTC |
| f3bc6c8 | Théo Winterhalter | 14 September 2019, 12:13:53 UTC | Remove zipx from safe conversion This allows for the removal of an untrue axiom. | 15 September 2019, 14:07:42 UTC |
| 9eef32e | Matthieu Sozeau | 15 September 2019, 10:23:39 UTC | Add an Acc_intro generator in safe reduction to try and run it inside Coq using lazy evaluation | 15 September 2019, 10:23:39 UTC |
| 4daf5b0 | Matthieu Sozeau | 15 September 2019, 10:20:07 UTC | install target requires all | 15 September 2019, 10:20:07 UTC |
| be7c281 | Matthieu Sozeau | 15 September 2019, 10:19:20 UTC | Put back Set Keyed Unification in PCUICSigmaCalculus, for fixed verion of Equations. | 15 September 2019, 10:19:20 UTC |
| 9fed601 | Matthieu Sozeau | 13 September 2019, 16:07:02 UTC | Fix erasure/safechecker hack to make a correct global environment (w.r.t universes), which was buggy. | 13 September 2019, 16:07:02 UTC |
| 6a98a75 | Théo Winterhalter | 13 September 2019, 15:28:51 UTC | Merge pull request #273 from MetaCoq/fix-conversion Fix conversion by changing its spec | 13 September 2019, 15:28:51 UTC |
| 77a3dbe | Théo Winterhalter | 13 September 2019, 14:48:27 UTC | Merge remote-tracking branch 'Template-Coq/coq-8.8' into fix-conversion | 13 September 2019, 14:48:27 UTC |
| e213597 | SimonBoulier | 13 September 2019, 09:54:48 UTC | Fix the SafeChecker with type_Case_valid_btys | 13 September 2019, 13:57:41 UTC |
| f9ab3e4 | SimonBoulier | 12 September 2019, 15:06:43 UTC | isWfArity_red | 13 September 2019, 13:57:41 UTC |
| 3c7c89a | SimonBoulier | 12 September 2019, 15:06:09 UTC | Admitted -> Qed in Confluence | 13 September 2019, 13:57:41 UTC |
| be5d977 | SimonBoulier | 12 September 2019, 10:39:04 UTC | Small lemma about levels | 13 September 2019, 13:57:41 UTC |
| 73e6654 | Théo Winterhalter | 13 September 2019, 13:27:58 UTC | Fix post-merge | 13 September 2019, 13:49:08 UTC |
| 8ba4e8b | Théo Winterhalter | 13 September 2019, 11:11:18 UTC | Merge remote-tracking branch 'Template-Coq/coq-8.8' into fix-conversion | 13 September 2019, 11:11:18 UTC |
| 910e78a | Théo Winterhalter | 12 September 2019, 15:10:35 UTC | Fix conversion by changing its spec | 13 September 2019, 10:07:37 UTC |
| 32733a6 | SimonBoulier | 11 September 2019, 16:34:42 UTC | A few conv lemmas in SafeLemmata | 12 September 2019, 10:18:30 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 |
| 33b7456 | Matthieu Sozeau | 10 September 2019, 14:32:46 UTC | Add new safe erasure function for well-typed terms (avoiding recomputation of whole typings at every step) | 11 September 2019, 14:48:33 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 |
| 1647e10 | Matthieu Sozeau | 10 September 2019, 10:11:04 UTC | WIP on safe retyping | 10 September 2019, 14:25:56 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 |
