| b4c8c44 | Matthieu Sozeau | 25 July 2019, 06:14:10 UTC | Completing the Conversion file | 25 July 2019, 06:14:10 UTC |
| 5174c8f | Matthieu Sozeau | 25 July 2019, 05:30:35 UTC | We use bashisms in the extraction scripts | 25 July 2019, 05:30:35 UTC |
| 66c86ef | Matthieu Sozeau | 25 July 2019, 05:13:24 UTC | Use the right flags in the extracted erasure and add more tests | 25 July 2019, 05:13:24 UTC |
| 9fb99ee | Matthieu Sozeau | 25 July 2019, 05:08:40 UTC | Add .merlin targets to the Makefiles | 25 July 2019, 05:08:40 UTC |
| d76fd99 | Matthieu Sozeau | 25 July 2019, 05:05:02 UTC | Disable universe checking in the extracted checker for now. That doesn't really help though | 25 July 2019, 05:05:02 UTC |
| ad89e57 | Matthieu Sozeau | 25 July 2019, 05:01:25 UTC | Play more with erasure tests, it works! (as long as we don't use universes) | 25 July 2019, 05:01:25 UTC |
| f15a729 | Matthieu Sozeau | 25 July 2019, 04:30:06 UTC | Add and extract pretty-printers for all languages | 25 July 2019, 04:57:46 UTC |
| 35fb4f7 | Matthieu Sozeau | 25 July 2019, 03:47:05 UTC | Running the verified extracted erasure. | 25 July 2019, 03:47:05 UTC |
| 5ea4c1a | Matthieu Sozeau | 25 July 2019, 02:54:03 UTC | Minor compilation fixes, and building of the erasure plugin in progress. | 25 July 2019, 02:54:03 UTC |
| 441bf9e | Matthieu Sozeau | 25 July 2019, 02:32:38 UTC | Build erasure plugin, move printer to template-coq/AstUtils | 25 July 2019, 02:33:58 UTC |
| e87cff4 | Matthieu Sozeau | 25 July 2019, 02:07:13 UTC | Finally running the extracted code from the safe checker! | 25 July 2019, 02:07:13 UTC |
| f4a0ed0 | Matthieu Sozeau | 24 July 2019, 23:58:41 UTC | Need PCUICInduction in pcuic plugin | 24 July 2019, 23:58:41 UTC |
| c8b2df0 | Matthieu Sozeau | 24 July 2019, 23:56:57 UTC | Merge remote-tracking branch 'origin/coq-8.8' into extraction_new | 24 July 2019, 23:56:57 UTC |
| 00f7517 | Matthieu Sozeau | 24 July 2019, 23:55:21 UTC | Building the safe checker | 24 July 2019, 23:55:37 UTC |
| 0fb0759 | Matthieu Sozeau | 24 July 2019, 23:19:50 UTC | Changes in plugin compilation. Give up on separate pcuic/safechecker/erasure compilation | 24 July 2019, 23:24:36 UTC |
| e157211 | Matthieu Sozeau | 24 July 2019, 21:53:06 UTC | Fix PCUICSafeChecker for extraction (Prop/Type template problem) | 24 July 2019, 21:53:06 UTC |
| 6d415bd | Matthieu Sozeau | 24 July 2019, 21:38:19 UTC | Compilation fixes | 24 July 2019, 21:38:44 UTC |
| 7e4dd75 | Matthieu Sozeau | 24 July 2019, 21:38:03 UTC | Rename extraction module into erasure module | 24 July 2019, 21:38:03 UTC |
| aceca47 | Matthieu Sozeau | 24 July 2019, 21:17:23 UTC | Adapt erasure to refactorings | 24 July 2019, 21:18:03 UTC |
| a9a9ad8 | Matthieu Sozeau | 24 July 2019, 21:03:18 UTC | More refactorings and cleanups, remove one admit on conv_context_conversion | 24 July 2019, 21:03:18 UTC |
| 9e7c19e | Matthieu Sozeau | 24 July 2019, 18:14:57 UTC | Move utility functions and EAstUtils functions to their right place | 24 July 2019, 18:14:57 UTC |
| f24a16e | Matthieu Sozeau | 24 July 2019, 17:58:48 UTC | Merge pull request #242 from yforster/extraction_new Optimising erasure function and some fixed admits | 24 July 2019, 17:58:48 UTC |
| 0455731 | Matthieu Sozeau | 24 July 2019, 14:23:35 UTC | Merge pull request #241 from MetaCoq/extraction-arity Fix arity of Ret for extraction | 24 July 2019, 14:23:35 UTC |
| bb6d6f7 | Yannick Forster | 24 July 2019, 13:43:02 UTC | optimising erasure function | 24 July 2019, 13:43:02 UTC |
| 8167503 | Théo Winterhalter | 24 July 2019, 12:22:16 UTC | Fix arity of Ret for extraction | 24 July 2019, 13:04:48 UTC |
| 5bc2f4e | Yannick Forster | 23 July 2019, 14:49:26 UTC | Fixed admits regarding new eval rule for box | 23 July 2019, 14:49:26 UTC |
| 1a6eb9c | Yannick Forster | 23 July 2019, 13:34:10 UTC | Merge remote-tracking branch 'origin/coq-8.8' into extraction_new | 23 July 2019, 13:34:10 UTC |
| ce68941 | Matthieu Sozeau | 23 July 2019, 01:32:49 UTC | Fix the rest of the erasure proof. Admits because box reduction rule has changed We know ask for the argument of box to have a reduced form as well (as is done in CertiCoq also). I believe that does not change much and one can prove that the reduction is unnecessary. | 23 July 2019, 01:53:21 UTC |
| e914dcc | Matthieu Sozeau | 23 July 2019, 01:11:16 UTC | Improved wcbvEval relation in extraction. Avoids all unnecessary uses of mkApps | 23 July 2019, 01:11:16 UTC |
| 0d57343 | Matthieu Sozeau | 19 July 2019, 21:03:36 UTC | Merge pull request #235 from MetaCoq/invlet Inversions of let, prod, sorts for cumulativity | 19 July 2019, 21:03:36 UTC |
| 749311e | Matthieu Sozeau | 19 July 2019, 20:45:46 UTC | Remove guard-checking hypothesis in reduction of fix in extraction. | 19 July 2019, 20:45:46 UTC |
| c3e9542 | Matthieu Sozeau | 19 July 2019, 18:35:50 UTC | Prove inversion lemmas for LetIn (using reductions, not singling out the cases of no reduction) | 19 July 2019, 20:35:19 UTC |
| db5bcd1 | Matthieu Sozeau | 19 July 2019, 15:46:30 UTC | Prove the right inversion lemmas in PCUICConversion, checked that conv_conv_alt is actually not needed anywhere! | 19 July 2019, 15:46:30 UTC |
| d50d22c | Matthieu Sozeau | 19 July 2019, 13:54:44 UTC | Merge pull request #232 from MetaCoq/separate-plugin-compilation Separate plugin compilation | 19 July 2019, 13:54:44 UTC |
| f48b1a8 | Matthieu Sozeau | 19 July 2019, 13:25:37 UTC | Be explicit about the order of compilation of the live template plugin files | 19 July 2019, 13:25:37 UTC |
| 3e92060 | Matthieu Sozeau | 19 July 2019, 13:16:08 UTC | Build Template.All after Template.Loader | 19 July 2019, 13:16:08 UTC |
| 5da76e0 | Matthieu Sozeau | 19 July 2019, 13:09:34 UTC | Fix template and checker Loader and All files to run test-suite | 19 July 2019, 13:09:34 UTC |
| cbd70d0 | Théo Winterhalter | 19 July 2019, 12:46:28 UTC | Merge pull request #233 from yforster/fix-erasure Fixed admits in erasure introduced by #230 | 19 July 2019, 12:46:28 UTC |
| 905259b | Yannick Forster | 19 July 2019, 12:27:13 UTC | Fixed admits in erasure | 19 July 2019, 12:27:13 UTC |
| 09f8d44 | Matthieu Sozeau | 19 July 2019, 05:34:01 UTC | Put template_coq.cmx* in build/ too | 19 July 2019, 05:34:01 UTC |
| b42e62e | Matthieu Sozeau | 19 July 2019, 05:22:47 UTC | Change the _CoqProject.in NOT the _CoqProject... | 19 July 2019, 05:22:47 UTC |
| 4f5679e | Matthieu Sozeau | 19 July 2019, 05:05:00 UTC | Put uGraph and wGraph in the right order in the _CoqProject file?? | 19 July 2019, 05:05:00 UTC |
| 707df2d | Matthieu Sozeau | 19 July 2019, 05:03:37 UTC | Try to play more with dependencies | 19 July 2019, 05:03:37 UTC |
| 6551faa | Matthieu Sozeau | 19 July 2019, 02:32:21 UTC | More precise dependencies in uGraph.v so as not to let make build things in parallel when they shouldn't be! | 19 July 2019, 02:32:21 UTC |
| 52bd0c0 | Matthieu Sozeau | 19 July 2019, 01:50:10 UTC | Force building the .ml files before the Loader.v file for the template-coq plugin | 19 July 2019, 01:50:10 UTC |
| 54965e7 | Matthieu Sozeau | 19 July 2019, 01:41:36 UTC | Fix extraction includes as well | 19 July 2019, 01:41:36 UTC |
| 3792ee3 | Matthieu Sozeau | 19 July 2019, 01:18:41 UTC | Fix dependencies of PCUIC | 19 July 2019, 01:26:10 UTC |
| fd2808e | Matthieu Sozeau | 19 July 2019, 01:11:39 UTC | Move Induction, LiftSubst and UnivSubst back to template module: they are really important functions there. | 19 July 2019, 01:11:39 UTC |
| 1ca3c63 | Matthieu Sozeau | 19 July 2019, 01:04:33 UTC | Finally made checker separately compile from Template | 19 July 2019, 01:05:01 UTC |
| 793a036 | Matthieu Sozeau | 19 July 2019, 00:24:09 UTC | Add -bin-annot option | 19 July 2019, 00:24:09 UTC |
| a0f71d5 | Matthieu Sozeau | 19 July 2019, 00:18:36 UTC | Fix makefiles | 19 July 2019, 00:18:36 UTC |
| e0ef227 | Matthieu Sozeau | 18 July 2019, 22:34:49 UTC | Fix template-coq compilation: we have two plugins really | 18 July 2019, 22:34:49 UTC |
| 839a47b | Matthieu Sozeau | 16 July 2019, 17:58:28 UTC | Renamings, and different qualifications | 18 July 2019, 22:14:45 UTC |
| b43ef82 | Matthieu Sozeau | 16 July 2019, 17:44:47 UTC | Move template-coq typing development to the checker folder | 18 July 2019, 22:13:55 UTC |
| f2c1e4a | Matthieu Sozeau | 18 July 2019, 16:40:24 UTC | Merge pull request #230 from MetaCoq/context-conversion-and-refactor Context conversion and refactor | 18 July 2019, 16:40:24 UTC |
| 0d3e98c | Matthieu Sozeau | 18 July 2019, 16:14:18 UTC | Forgot a file in the .in | 18 July 2019, 16:14:18 UTC |
| 6519eb8 | Matthieu Sozeau | 18 July 2019, 15:46:54 UTC | Fix the checker makefile | 18 July 2019, 15:58:03 UTC |
| 14d8ae3 | Matthieu Sozeau | 18 July 2019, 15:27:44 UTC | Move patching after lowercasing of files | 18 July 2019, 15:27:44 UTC |
| a32d448 | Matthieu Sozeau | 18 July 2019, 14:55:52 UTC | Patch extraction of eq_equivalence | 18 July 2019, 14:55:52 UTC |
| 989c472 | Matthieu Sozeau | 18 July 2019, 14:46:10 UTC | Update .gitignore | 18 July 2019, 14:46:10 UTC |
| 644b980 | Matthieu Sozeau | 18 July 2019, 04:08:57 UTC | Fix compilation of checker and pcuic plugins that depend on each other | 18 July 2019, 04:08:57 UTC |
| 53f9bb5 | Matthieu Sozeau | 18 July 2019, 04:01:25 UTC | Adapted extraction to the use of == in place of = and a weaker context_conversion relation. Just one admit introduced that should be provable about well-formed contexts of fixpoints but I'm tired :) | 18 July 2019, 04:01:25 UTC |
| 5673fc0 | Matthieu Sozeau | 18 July 2019, 02:38:26 UTC | Adapt safe conversion to new interface of conv. | 18 July 2019, 02:45:13 UTC |
| 387ac72 | Matthieu Sozeau | 18 July 2019, 01:31:00 UTC | Fix template-coq plugin compilation | 18 July 2019, 01:31:00 UTC |
| 52aa7a1 | Matthieu Sozeau | 18 July 2019, 00:43:27 UTC | Fix plugin compilation (another bug in extraction found) | 18 July 2019, 00:43:27 UTC |
| 8d4e728 | Matthieu Sozeau | 18 July 2019, 00:32:46 UTC | Adapt later files to refactorings. Done with .v's here! | 18 July 2019, 00:32:46 UTC |
| faec213 | Matthieu Sozeau | 18 July 2019, 00:11:01 UTC | Refactorings and cleanups in higher files: add PCUICContextConversion Also change a lot of lemmas to use the == conversion relation instead of = | 18 July 2019, 00:11:01 UTC |
| ecaccc5 | Matthieu Sozeau | 17 July 2019, 21:12:45 UTC | Move instances of Equivalence eq_term and PartialOrder eq_term leq_term to PCUICEquality | 17 July 2019, 21:12:45 UTC |
| a58338d | Matthieu Sozeau | 17 July 2019, 21:12:34 UTC | Fix wrong coercion in PCUICTyping | 17 July 2019, 21:12:34 UTC |
| 19dd216 | Matthieu Sozeau | 17 July 2019, 20:29:03 UTC | Show eq_term antisymmetry and refactor in PCUICCumulativity | 17 July 2019, 20:29:03 UTC |
| 52c0a74 | Matthieu Sozeau | 17 July 2019, 20:26:28 UTC | Refactorings and coercion declarations in PCUICTyping for constraints out of environments/environments extensions | 17 July 2019, 20:28:43 UTC |
| 11d6ddc | Matthieu Sozeau | 17 July 2019, 19:56:03 UTC | Refactor in Equality | 17 July 2019, 19:56:03 UTC |
| f86e3a6 | Matthieu Sozeau | 17 July 2019, 19:39:13 UTC | Show antisymmetry of leq_universes w.r.t. eq_universes and add TC instances for reflexivity, symmetry etc.. | 17 July 2019, 19:43:07 UTC |
| 87c4bc6 | Matthieu Sozeau | 17 July 2019, 19:16:02 UTC | WIP in PCUICConversion (dirty) | 17 July 2019, 19:18:10 UTC |
| 19e24f2 | Matthieu Sozeau | 16 July 2019, 17:07:28 UTC | WIP on cumul and confluence lemmas | 17 July 2019, 19:18:10 UTC |
| 449d876 | Matthieu Sozeau | 15 July 2019, 20:02:20 UTC | Almost there with cumulativity / conversion alternative version. | 17 July 2019, 19:18:10 UTC |
| 97cc488 | Matthieu Sozeau | 16 July 2019, 23:47:48 UTC | Simplify proofs in PCUICEquality thanks to a symmetry argument | 17 July 2019, 19:18:10 UTC |
| 1f44b77 | Théo Winterhalter | 16 July 2019, 09:40:09 UTC | Merge pull request #228 from MetaCoq/cumul-confluence Cumul confluence | 16 July 2019, 09:40:09 UTC |
| e7a46c0 | Théo Winterhalter | 16 July 2019, 08:39:08 UTC | Merge branch 'coq-8.8' into cumul-confluence | 16 July 2019, 08:39:08 UTC |
| 7488a35 | Théo Winterhalter | 15 July 2019, 15:25:47 UTC | Fix extraction | 15 July 2019, 15:25:47 UTC |
| 9466c21 | Théo Winterhalter | 15 July 2019, 14:55:01 UTC | Fix SafeChecker | 15 July 2019, 14:55:01 UTC |
| 06fadcb | Théo Winterhalter | 15 July 2019, 14:17:28 UTC | Fix SafeConversion | 15 July 2019, 14:17:28 UTC |
| 9b3d593 | Théo Winterhalter | 15 July 2019, 13:49:45 UTC | Fix Elimination and SafeReduce, partial fix of SafeConversion | 15 July 2019, 13:49:45 UTC |
| b5f582a | Théo Winterhalter | 15 July 2019, 12:35:34 UTC | Fix SafeLemmata | 15 July 2019, 12:35:34 UTC |
| 8a4c5f5 | Théo Winterhalter | 15 July 2019, 08:49:49 UTC | Fix welltyped_context and wellformed_context Not enough, now a lot of properties require `wf Σ`. | 15 July 2019, 08:50:25 UTC |
| 40e0015 | Matthieu Sozeau | 15 July 2019, 07:40:37 UTC | Renamings and progress in conversion | 15 July 2019, 08:03:30 UTC |
| 64f0fe9 | Théo Winterhalter | 12 July 2019, 19:52:37 UTC | Merge pull request #227 from MetaCoq/readme Sort remaining files in PCUIC readme | 12 July 2019, 19:52:37 UTC |
| 61bff76 | Théo Winterhalter | 12 July 2019, 19:51:40 UTC | Sort remaining files in PCUIC readme | 12 July 2019, 19:51:45 UTC |
| 0703159 | Théo Winterhalter | 12 July 2019, 18:58:13 UTC | Merge pull request #226 from MetaCoq/readme Improve READMEs | 12 July 2019, 18:58:13 UTC |
| 45818aa | Théo Winterhalter | 12 July 2019, 18:57:39 UTC | Largely improve README for PCUIC | 12 July 2019, 18:57:39 UTC |
| 37ff3cc | Théo Winterhalter | 12 July 2019, 18:28:20 UTC | Merge pull request #225 from MetaCoq/construct-ind-eq Trying to prove Construct_ind_eq and other stuff | 12 July 2019, 18:28:20 UTC |
| b3715a2 | Matthieu Sozeau | 12 July 2019, 17:41:06 UTC | Renamings and WIP proving confluence of red1 + leq_term | 12 July 2019, 17:41:06 UTC |
| cbc6b90 | Théo Winterhalter | 12 July 2019, 17:02:42 UTC | Some refactoring | 12 July 2019, 17:17:28 UTC |
| 25f9f8c | Théo Winterhalter | 12 July 2019, 14:35:12 UTC | Uniformise invert_cumul_ind_l and _r, removing some duplicates | 12 July 2019, 14:35:12 UTC |
| 884d510 | Théo Winterhalter | 12 July 2019, 12:50:36 UTC | Add readme for PCUIC (wip) | 12 July 2019, 12:50:36 UTC |
| 92c8daf | Théo Winterhalter | 12 July 2019, 12:18:06 UTC | Add README for Safe Checker | 12 July 2019, 12:18:06 UTC |
| 7da5285 | Théo Winterhalter | 12 July 2019, 12:01:17 UTC | Add quick jumps and safe checker to README | 12 July 2019, 12:01:17 UTC |
| 6b96be5 | Théo Winterhalter | 12 July 2019, 11:41:38 UTC | Prove invert_cumul_ind_r | 12 July 2019, 11:41:38 UTC |
| 68aeab9 | Théo Winterhalter | 12 July 2019, 09:44:37 UTC | Fail to prove Construct_Ind_ind_eq | 12 July 2019, 09:44:37 UTC |
| 6417e3f | Théo Winterhalter | 12 July 2019, 08:59:57 UTC | Failed attempt at inversion_mkApps | 12 July 2019, 08:59:57 UTC |
