| 1887074 | Matthieu Sozeau | 20 September 2019, 11:28:28 UTC | Commit HTML doc | 20 September 2019, 11:28:28 UTC |
| 97d3513 | Matthieu Sozeau | 20 September 2019, 11:20:49 UTC | Add warning about previous installation | 20 September 2019, 11:20:49 UTC |
| ed065ff | Matthieu Sozeau | 20 September 2019, 11:15:15 UTC | Remove obsolete file | 20 September 2019, 11:15:15 UTC |
| fea05ac | Matthieu Sozeau | 20 September 2019, 11:07:46 UTC | Update README-material | 20 September 2019, 11:09:27 UTC |
| 322801f | Matthieu Sozeau | 20 September 2019, 10:59:59 UTC | Fixed html target | 20 September 2019, 11:09:27 UTC |
| edd4c51 | Matthieu Sozeau | 20 September 2019, 10:55:05 UTC | Updated README-MATERIAL file | 20 September 2019, 11:09:27 UTC |
| beff30c | Matthieu Sozeau | 20 September 2019, 10:47:54 UTC | Update README.md to refer to clean branch instead | 20 September 2019, 11:09:27 UTC |
| d02b365 | Théo Winterhalter | 20 September 2019, 09:51:01 UTC | Remove axiom Proj_red_cond Reduction just has an inaccessible branch now. | 20 September 2019, 11:09:27 UTC |
| 26411b6 | Théo Winterhalter | 20 September 2019, 09:05:34 UTC | Remove Construct_Ind_ind_eq axiom This implies making the checker check for more things | 20 September 2019, 11:09:27 UTC |
| e8a769c | Théo Winterhalter | 20 September 2019, 08:59:51 UTC | Import ContextConversion to remove full qualid in Print Assumptions | 20 September 2019, 11:09:27 UTC |
| f3850da | Matthieu Sozeau | 20 September 2019, 11:08:32 UTC | Merge pull request #271 from yforster/remove_case_optimisations Remove case optimisations and fix regressions in erasure | 20 September 2019, 11:08:32 UTC |
| ffc322b | Matthieu Sozeau | 20 September 2019, 10:10:56 UTC | Merge branch 'coq-8.8' into remove_case_optimisations | 20 September 2019, 10:10:56 UTC |
| a710009 | Matthieu Sozeau | 20 September 2019, 09:56:57 UTC | Merge pull request #294 from MetaCoq/erase-timing Erase timing | 20 September 2019, 09:56:57 UTC |
| c8fc338 | Yannick Forster | 20 September 2019, 09:33:04 UTC | no admits | 20 September 2019, 09:33:04 UTC |
| 28bbbb7 | Matthieu Sozeau | 20 September 2019, 08:53:48 UTC | Fix Makefile dependencies for test-suite, add vs example from CertiCoq | 20 September 2019, 09:32:31 UTC |
| 32bdca8 | Yannick Forster | 20 September 2019, 09:27:17 UTC | this version is provable | 20 September 2019, 09:27:17 UTC |
| efca71f | Yannick Forster | 20 September 2019, 09:17:19 UTC | fixed compilation | 20 September 2019, 09:17:19 UTC |
| 70c6b54 | Yannick Forster | 20 September 2019, 09:02:42 UTC | Merge remote-tracking branch 'origin/coq-8.8' into remove_case_optimisations | 20 September 2019, 09:02:42 UTC |
| af1e517 | Yannick Forster | 20 September 2019, 08:55:23 UTC | One lemma missing, then erasure is finished again | 20 September 2019, 08:55:23 UTC |
| 50c707b | Matthieu Sozeau | 20 September 2019, 08:35:50 UTC | Timing info in MetaCoq Erase as well and add safechecker_test and erasure_test to the test-suite build | 20 September 2019, 08:41:33 UTC |
| f4cbdf3 | Matthieu Sozeau | 20 September 2019, 08:27:43 UTC | Timing info in MetaCoq CoqCheck and SafeCheck | 20 September 2019, 08:27:59 UTC |
| e6c70ee | Matthieu Sozeau | 20 September 2019, 08:27:23 UTC | Merge pull request #286 from MetaCoq/unsafe-checker Unsafe checker | 20 September 2019, 08:27:23 UTC |
| 4ab5ec0 | Yannick Forster | 20 September 2019, 07:38:17 UTC | Fix all universe issues | 20 September 2019, 07:38:17 UTC |
| 1ae81f0 | Matthieu Sozeau | 20 September 2019, 07:28:29 UTC | Remove ast_id_quoter | 20 September 2019, 07:28:29 UTC |
| 138523e | Théo Winterhalter | 18 September 2019, 14:37:55 UTC | Unsafe checker command running. We don't get inductive dependencies yet. | 20 September 2019, 07:18:18 UTC |
| 5aa4b46 | Théo Winterhalter | 19 September 2019, 10:18:10 UTC | Add HoTT test for checker | 20 September 2019, 07:17:52 UTC |
| 180899d | Théo Winterhalter | 19 September 2019, 10:17:59 UTC | Dummy version of unsafe checker | 20 September 2019, 07:16:55 UTC |
| 27ae1a6 | Théo Winterhalter | 18 September 2019, 14:37:55 UTC | WIP unsafe checker command | 20 September 2019, 07:16:55 UTC |
| 8cd855e | Matthieu Sozeau | 20 September 2019, 07:08:49 UTC | Merge pull request #292 from MetaCoq/fix-opam-install Fix opam install | 20 September 2019, 07:08:49 UTC |
| da32cdb | Yannick Forster | 20 September 2019, 06:48:14 UTC | fix compilation | 20 September 2019, 06:48:14 UTC |
| d69b84f | Matthieu Sozeau | 19 September 2019, 22:27:54 UTC | Update travis config and toplevel Makefile to test opam install | 20 September 2019, 06:41:32 UTC |
| 53f9703 | Yannick Forster | 20 September 2019, 06:32:24 UTC | Merge remote-tracking branch 'origin/univ_subst_wk' into remove_case_optimisations | 20 September 2019, 06:32:24 UTC |
| 87a6baf | Théo Winterhalter | 19 September 2019, 22:58:37 UTC | Merge pull request #291 from MetaCoq/conversion-unfold Unfold constants more in safe conversion | 19 September 2019, 22:58:37 UTC |
| e26ae65 | Matthieu Sozeau | 19 September 2019, 22:09:40 UTC | Qualify Template/Checker imports more precisely | 19 September 2019, 22:09:40 UTC |
| 758f11a | Théo Winterhalter | 19 September 2019, 21:36:39 UTC | Unfold constants more in safe conversion | 19 September 2019, 21:40:37 UTC |
| c502a6a | Théo Winterhalter | 19 September 2019, 21:18:44 UTC | Merge pull request #290 from MetaCoq/conversion-fix Change checker printing a bit for clarity | 19 September 2019, 21:18:44 UTC |
| 8069f04 | Théo Winterhalter | 19 September 2019, 20:55:46 UTC | Readd parentheses around rhs of application | 19 September 2019, 20:55:46 UTC |
| 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 |
| 69ca2aa | Théo Winterhalter | 19 September 2019, 20:39:20 UTC | Merge pull request #288 from MetaCoq/conversion-fix Add missing case on conversion fallback | 19 September 2019, 20:39:20 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 |
| a3c47d0 | Matthieu Sozeau | 19 September 2019, 15:44:15 UTC | Merge pull request #284 from yforster/configure-for-opam Add configure.sh to opam files | 19 September 2019, 15:44:15 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 |
| e74add0 | Matthieu Sozeau | 19 September 2019, 10:38:28 UTC | Fix compile time dependencies of plugins in global and local installation mode | 19 September 2019, 14:54:47 UTC |
| f33d84a | SimonBoulier | 19 September 2019, 13:11:05 UTC | Weaken the assumptions in UnivSubst lemmas | 19 September 2019, 14:17:53 UTC |
| f54fa89 | Yannick Forster | 19 September 2019, 14:11:01 UTC | fix erasure test-suite for now | 19 September 2019, 14:11:01 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 |
| 23da953 | Yannick Forster | 19 September 2019, 14:06:35 UTC | Finished fix unfolding | 19 September 2019, 14:06:35 UTC |
| 30ca9f4 | SimonBoulier | 19 September 2019, 13:11:05 UTC | Weaken the assumptions in UnivSubst lemmas | 19 September 2019, 13:11:05 UTC |
| 6cd59a2 | Yannick Forster | 19 September 2019, 10:43:20 UTC | add partial decider for irreducibility | 19 September 2019, 10:43:20 UTC |
| b24e072 | Matthieu Sozeau | 19 September 2019, 10:14:00 UTC | Apply Extraction -> erasure renaming everywhere | 19 September 2019, 10:19:31 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 |
| cd693e6 | Matthieu Sozeau | 19 September 2019, 09:34:09 UTC | Separate compilation fixes | 19 September 2019, 10:09:23 UTC |
| 1ae0d4a | Yannick Forster | 19 September 2019, 10:04:26 UTC | app cong case closed | 19 September 2019, 10:04:26 UTC |
| 6d75afa | Yannick Forster | 19 September 2019, 09:29:16 UTC | Progress in correctness proof, universe issues + app_cong + fixpoints missing | 19 September 2019, 09:29:16 UTC |
| 3f398d9 | Yannick Forster | 19 September 2019, 08:09:36 UTC | Add configure.sh to opam files | 19 September 2019, 08:09:36 UTC |
| bfb6dba | Yannick Forster | 19 September 2019, 06:04:37 UTC | Merge branch 'remove_case_optimisations' of github.com:yforster/template-coq into remove_case_optimisations | 19 September 2019, 06:04:37 UTC |
| 80b4455 | Yannick Forster | 19 September 2019, 06:04:25 UTC | Use decider for normality | 19 September 2019, 06:04:25 UTC |
| e55cdfd | Yannick Forster | 19 September 2019, 06:04:18 UTC | Merge pull request #6 from SimonBoulier/remove_case_optimisations fix isErasable_subst_instance | 19 September 2019, 06:04:18 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 |
| bafc088 | SimonBoulier | 18 September 2019, 10:13:22 UTC | fix isErasable_subst_instance | 18 September 2019, 10:13:22 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 |
| f454938 | Yannick Forster | 17 September 2019, 12:18:24 UTC | Add comments for Simon | 17 September 2019, 12:18:24 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 |
