| 2b6368c | SimonBoulier | 23 August 2019, 13:27:32 UTC | Remove useless plugin | 23 August 2019, 13:36:06 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 |
| 6e7b92e | Matthieu Sozeau | 30 July 2019, 03:27:50 UTC | Cleanup definition of wcbvEval in PCUIC and pull back to template-coq def | 30 July 2019, 03:29:34 UTC |
| 7353a2c | Matthieu Sozeau | 28 July 2019, 17:51:26 UTC | Merge pull request #239 from MetaCoq/extraction_new Erasure 2.0 | 28 July 2019, 17:51:26 UTC |
| 813613e | Matthieu Sozeau | 28 July 2019, 17:08:01 UTC | Adapt erasure to new wcbvEval. Admitted a few cases! | 28 July 2019, 17:08:01 UTC |
| a13317f | Théo Winterhalter | 27 July 2019, 13:21:15 UTC | Merge pull request #229 from MetaCoq/sigma-calculus Instantiation in σ-calculus | 27 July 2019, 13:21:15 UTC |
| 43cbfbf | Matthieu Sozeau | 26 July 2019, 22:38:55 UTC | Convert lemmas to ~~ foo instead of foo = false, as per ssr recommendations | 26 July 2019, 22:49:46 UTC |
| f2138f8 | Matthieu Sozeau | 26 July 2019, 18:36:49 UTC | WIP updating ParallelReduction | 26 July 2019, 18:36:49 UTC |
| 3d26785 | Matthieu Sozeau | 26 July 2019, 15:15:04 UTC | Updated WcbvEval relation in PCUIC, which features, compared to EwcbvEval: - mkApps for guarded fix reduction - Stuck fixpoint applications - Axioms are values - Local assumptions are values. The expectation is that all these can be ruled out/simulated through erasure due to typing constraints (no axioms in the global context and an empty local context), no undully stuck fixpoints. | 26 July 2019, 15:15:04 UTC |
| 0eb0f32 | Théo Winterhalter | 25 July 2019, 14:57:24 UTC | Merge remote-tracking branch 'Template-Coq/coq-8.8' into sigma-calculus | 25 July 2019, 14:57:24 UTC |
| 55909b0 | Théo Winterhalter | 25 July 2019, 14:57:06 UTC | Start with red1_rename | 25 July 2019, 14:57:06 UTC |
| cb79631 | Matthieu Sozeau | 25 July 2019, 13:22:47 UTC | Avoid relying on ocaml >= 4.07 library functions | 25 July 2019, 13:22:47 UTC |
| 735b954 | Théo Winterhalter | 25 July 2019, 12:48:40 UTC | Prove eq_term_upto_univ_rename | 25 July 2019, 12:48:40 UTC |
| 58edd8f | Théo Winterhalter | 25 July 2019, 10:10:50 UTC | Progress on cumulativity case in renaming | 25 July 2019, 10:10:50 UTC |
| fc7837b | Théo Winterhalter | 25 July 2019, 09:49:54 UTC | Complete projection renaming | 25 July 2019, 09:49:54 UTC |
| 7b61e5a | Théo Winterhalter | 25 July 2019, 09:33:00 UTC | Prove rename_subst0 | 25 July 2019, 09:33:00 UTC |
| 4c54169 | Théo Winterhalter | 25 July 2019, 08:52:26 UTC | Minor progress with projection renaming | 25 July 2019, 08:52:26 UTC |
| f9fc05f | Matthieu Sozeau | 25 July 2019, 06:33:12 UTC | Fix Makefile spaces to tabs | 25 July 2019, 06:33:12 UTC |
| 0abcb87 | Matthieu Sozeau | 25 July 2019, 05:30:35 UTC | We use bashisms in the extraction scripts | 25 July 2019, 06:31:26 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 |
| 7fefdf3 | Théo Winterhalter | 24 July 2019, 15:45:08 UTC | Deal with tConstruct case for rename | 24 July 2019, 15:45:08 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 |
| 96899b9 | Théo Winterhalter | 24 July 2019, 10:28:02 UTC | Deal with inductive type for typing_rename | 24 July 2019, 10:28:02 UTC |
| 7f7e0b5 | Théo Winterhalter | 24 July 2019, 09:57:00 UTC | Deal with constant for typing_rename | 24 July 2019, 09:57:00 UTC |
| d14aa11 | Théo Winterhalter | 23 July 2019, 15:12:11 UTC | Complete types_of_case_rename modulo branches | 23 July 2019, 15:12:11 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 |
| 2291e1c | Théo Winterhalter | 23 July 2019, 14:22:59 UTC | Define rename_context | 23 July 2019, 14:22:59 UTC |
| 996bd25 | Théo Winterhalter | 23 July 2019, 14:09:04 UTC | Move around stuff necessary for types_of_case | 23 July 2019, 14:09:59 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 |
| 13aa3b1 | Théo Winterhalter | 23 July 2019, 12:11:20 UTC | Prove rename_subst_instance_constr | 23 July 2019, 12:11:20 UTC |
| 11982c8 | Théo Winterhalter | 23 July 2019, 11:48:36 UTC | Add rewrite hint for lift_rename | 23 July 2019, 11:48:36 UTC |
| 3e35133 | Théo Winterhalter | 23 July 2019, 11:46:14 UTC | Prove subst1_inst | 23 July 2019, 11:46:14 UTC |
| 9f88150 | Théo Winterhalter | 23 July 2019, 09:43:12 UTC | Change renaming def and finally prove its properties | 23 July 2019, 09:43:12 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 |
| 9284c2d | Théo Winterhalter | 22 July 2019, 15:23:25 UTC | State renaming_vdef and placeholders for proof | 22 July 2019, 15:23:25 UTC |
| ef3d6b2 | Théo Winterhalter | 22 July 2019, 14:06:38 UTC | Big chunk of proof to do simple conversion | 22 July 2019, 14:06:38 UTC |
| 5ab2155 | Théo Winterhalter | 22 July 2019, 12:33:00 UTC | Not clear what is the right definition | 22 July 2019, 12:33:00 UTC |
| 2fb39f6 | Théo Winterhalter | 22 July 2019, 10:32:34 UTC | Yet another wrong def | 22 July 2019, 10:32:34 UTC |
| cc9b596 | Théo Winterhalter | 22 July 2019, 09:43:54 UTC | Update def of rename | 22 July 2019, 09:43:54 UTC |
| 092c6d1 | Théo Winterhalter | 22 July 2019, 08:55:31 UTC | First statement of renaming lemma | 22 July 2019, 08:55:31 UTC |
| cdc8dae | Théo Winterhalter | 20 July 2019, 16:14:15 UTC | Update def of well_subst | 20 July 2019, 16:14:15 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 |
| 8abfaab | Théo Winterhalter | 19 July 2019, 14:31:40 UTC | Complete types_of_case_inst modulo build_branches_type_inst | 19 July 2019, 14:31:40 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 |
| bfa26e5 | Théo Winterhalter | 19 July 2019, 12:04:45 UTC | Prove inst_destArity and more | 19 July 2019, 12:04:45 UTC |
| f6a39f0 | Théo Winterhalter | 19 July 2019, 09:40:58 UTC | Prove inst_declared_inductive (and more) | 19 July 2019, 09:40:58 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 |
