| 19d43e2 | Matthieu Sozeau | 05 July 2019, 16:30:28 UTC | WIP updating the proofs | 09 July 2019, 19:39:27 UTC |
| 4ba25d9 | Matthieu Sozeau | 04 July 2019, 06:14:31 UTC | Add fix/cofix checking | 09 July 2019, 19:20:49 UTC |
| 4980bf0 | Matthieu Sozeau | 09 July 2019, 18:41:11 UTC | Merge pull request #204 from MetaCoq/typing_globenv-rebase Rebase of #182 | 09 July 2019, 18:41:11 UTC |
| 290960e | Matthieu Sozeau | 09 July 2019, 18:14:41 UTC | Fix test-suite | 09 July 2019, 18:14:41 UTC |
| e4783e0 | Matthieu Sozeau | 09 July 2019, 18:04:06 UTC | Merge remote-tracking branch 'origin/coq-8.8' into typing_globenv-rebase2 | 09 July 2019, 18:04:06 UTC |
| f37d133 | Matthieu Sozeau | 09 July 2019, 17:40:10 UTC | Update Extraction. I did something wrong with the extends stuff I think, but should be easy to fix | 09 July 2019, 17:40:10 UTC |
| 03d25c3 | Matthieu Sozeau | 09 July 2019, 16:56:11 UTC | Fix admits in PCUICConfluence and PCUIC extraction, removing the hack about module path equality! | 09 July 2019, 16:56:11 UTC |
| fcd94a4 | Matthieu Sozeau | 09 July 2019, 15:58:48 UTC | Merge pull request #203 from MetaCoq/type-rename Move type_rename and begin proving it | 09 July 2019, 15:58:48 UTC |
| adfa70c | Théo Winterhalter | 09 July 2019, 15:42:17 UTC | Fix compilation again | 09 July 2019, 15:42:17 UTC |
| 2210df4 | Théo Winterhalter | 09 July 2019, 15:15:33 UTC | Add eq_term axiom for fix_guard | 09 July 2019, 15:15:33 UTC |
| c9d1bd1 | Théo Winterhalter | 09 July 2019, 15:13:28 UTC | Reorganise SafeLemmata, wf_nlg is harder than expected | 09 July 2019, 15:13:28 UTC |
| 2e2d2cb | Théo Winterhalter | 09 July 2019, 15:01:30 UTC | Fix compilation | 09 July 2019, 15:01:30 UTC |
| dfce5dc | Théo Winterhalter | 09 July 2019, 14:50:08 UTC | Almost done with type_rename | 09 July 2019, 14:50:08 UTC |
| 03787cb | SimonBoulier | 09 July 2019, 14:14:12 UTC | compiles upt to extraction of pcuic | 09 July 2019, 14:14:12 UTC |
| 9726394 | SimonBoulier | 09 July 2019, 12:59:21 UTC | Merge of typing_globenv | 09 July 2019, 13:49:41 UTC |
| a2c6e40 | Théo Winterhalter | 09 July 2019, 13:48:33 UTC | Fix context conversion | 09 July 2019, 13:48:33 UTC |
| 114883e | Théo Winterhalter | 09 July 2019, 13:08:22 UTC | Progress but need to fix conv_vdef_body | 09 July 2019, 13:08:22 UTC |
| 9303cfa | Théo Winterhalter | 09 July 2019, 12:00:20 UTC | Fix compilation | 09 July 2019, 12:00:20 UTC |
| 2575388 | Théo Winterhalter | 09 July 2019, 09:32:42 UTC | Move type_rename and begin proving it | 09 July 2019, 09:32:42 UTC |
| 6df3ede | Théo Winterhalter | 09 July 2019, 08:22:51 UTC | Merge pull request #202 from MetaCoq/more-eq More lemmata on `eq_term` | 09 July 2019, 08:22:51 UTC |
| bb9f75d | Théo Winterhalter | 09 July 2019, 07:33:08 UTC | Fix post merge | 09 July 2019, 07:56:20 UTC |
| 4904451 | Théo Winterhalter | 09 July 2019, 07:17:31 UTC | Merge remote-tracking branch 'Template-Coq/coq-8.8' into more-eq | 09 July 2019, 07:17:31 UTC |
| b97d46f | Matthieu Sozeau | 09 July 2019, 07:10:46 UTC | Fix plugin compilation | 09 July 2019, 07:10:46 UTC |
| d56ca30 | Matthieu Sozeau | 09 July 2019, 06:16:24 UTC | Fix template-coq scripts again?? | 09 July 2019, 06:16:24 UTC |
| 4361a40 | Matthieu Sozeau | 09 July 2019, 05:51:00 UTC | Fix extraction also | 09 July 2019, 05:51:00 UTC |
| 52fc0a3 | Matthieu Sozeau | 09 July 2019, 05:47:35 UTC | Update confluence also | 09 July 2019, 05:47:35 UTC |
| 4d172e9 | Matthieu Sozeau | 09 July 2019, 05:36:47 UTC | Progress in reproving template-to-pcuic | 09 July 2019, 05:36:47 UTC |
| dfda1c5 | Matthieu Sozeau | 09 July 2019, 00:31:10 UTC | WIP fixing compilation | 09 July 2019, 03:45:22 UTC |
| d535eb8 | Théo Winterhalter | 08 July 2019, 21:27:31 UTC | Move OnOne2_impl_exist_and_All_r in utils | 08 July 2019, 21:27:31 UTC |
| 7a3f466 | Théo Winterhalter | 08 July 2019, 21:25:03 UTC | Prove red1_eq_term_upto_univ_r | 08 July 2019, 21:25:03 UTC |
| 8ca01fe | Théo Winterhalter | 08 July 2019, 20:58:21 UTC | State and prove red1_eq_context_upto_r | 08 July 2019, 20:58:21 UTC |
| 90f3e84 | Matthieu Sozeau | 08 July 2019, 20:46:07 UTC | Fix compilation | 08 July 2019, 20:46:07 UTC |
| 3918fc1 | Théo Winterhalter | 08 July 2019, 19:01:28 UTC | Progress with red1_eq_term_upto_univ_r | 08 July 2019, 19:04:34 UTC |
| e3220ff | Théo Winterhalter | 08 July 2019, 17:52:17 UTC | Add isConstruct_app_eq_term_r | 08 July 2019, 17:52:17 UTC |
| cf06831 | Théo Winterhalter | 08 July 2019, 17:49:40 UTC | Add isLambda_eq_term_r | 08 July 2019, 17:49:40 UTC |
| 71c69c9 | Théo Winterhalter | 08 July 2019, 17:41:18 UTC | Prove All2_nth_error_Some_r and eq_term_upto_univ_mkApps_r_inv | 08 July 2019, 17:41:18 UTC |
| 2834ee0 | Théo Winterhalter | 08 July 2019, 15:58:50 UTC | Restate red1_eq_term_upto_univ_r | 08 July 2019, 16:11:37 UTC |
| 5a0f865 | Matthieu Sozeau | 08 July 2019, 15:46:39 UTC | Merge pull request #201 from TheoWinterhalter/guard Add guard conditions to PCUIC | 08 July 2019, 15:46:39 UTC |
| 78b6a91 | Théo Winterhalter | 08 July 2019, 14:17:12 UTC | Extract Constant corresponding to guards | 08 July 2019, 15:18:48 UTC |
| b428318 | Théo Winterhalter | 08 July 2019, 11:33:45 UTC | Add guard conditions to TemplateCoq | 08 July 2019, 15:18:48 UTC |
| 01bcca3 | Théo Winterhalter | 08 July 2019, 09:56:47 UTC | Add guard conditions to PCUIC | 08 July 2019, 15:18:48 UTC |
| 9f79616 | Théo Winterhalter | 08 July 2019, 15:18:00 UTC | State red1_eq_term_upto_univ_r | 08 July 2019, 15:18:00 UTC |
| 22870f5 | Matthieu Sozeau | 08 July 2019, 15:12:06 UTC | Merge pull request #199 from MetaCoq/context_conversion Context conversion | 08 July 2019, 15:12:06 UTC |
| 1e7ef5a | Théo Winterhalter | 08 July 2019, 14:57:54 UTC | Prove eq_universe_sym and eq_term_sym | 08 July 2019, 14:57:54 UTC |
| f5f9537 | Théo Winterhalter | 08 July 2019, 14:44:05 UTC | Prove eq_term_upto_univ_sym | 08 July 2019, 14:44:05 UTC |
| 13bde9c | Matthieu Sozeau | 08 July 2019, 14:07:12 UTC | Adapt extraction to changes in Validity/SR | 08 July 2019, 14:07:12 UTC |
| 4f628f2 | Théo Winterhalter | 08 July 2019, 13:09:53 UTC | Weaken type_rename to be exact on sorts And update in accordance. | 08 July 2019, 13:53:52 UTC |
| 072f2cc | Théo Winterhalter | 08 July 2019, 08:21:30 UTC | Move admitted type_rename and deduce type_nameless from it | 08 July 2019, 08:21:30 UTC |
| bca1006 | Matthieu Sozeau | 08 July 2019, 03:43:39 UTC | Finished proving context conversion up-to a believable lemma about red and eq-universes | 08 July 2019, 04:02:45 UTC |
| f1a76b3 | Matthieu Sozeau | 07 July 2019, 23:27:52 UTC | Moving eq lemmata to Type and refactorings | 08 July 2019, 03:43:36 UTC |
| c2a879d | Matthieu Sozeau | 07 July 2019, 20:44:14 UTC | WIP moving eq_context_upto lemmas to Type | 07 July 2019, 21:24:17 UTC |
| 9b5cd1a | Matthieu Sozeau | 07 July 2019, 20:21:10 UTC | Update confluence to be up-to renamings in contexts | 07 July 2019, 20:32:53 UTC |
| 9615062 | Matthieu Sozeau | 07 July 2019, 08:41:58 UTC | Minor refactorings and fixups to make everything compile again | 07 July 2019, 20:32:53 UTC |
| c3ee8e1 | Matthieu Sozeau | 07 July 2019, 08:11:44 UTC | Proved most of context conversion for red/conv/cumul and typing! | 07 July 2019, 20:32:33 UTC |
| 81b5e44 | Matthieu Sozeau | 07 July 2019, 19:20:34 UTC | Merge pull request #198 from MetaCoq/red1-eq-term Prove red1_eq_term_upto_univ_l | 07 July 2019, 19:20:34 UTC |
| d772bf0 | Théo Winterhalter | 07 July 2019, 18:04:22 UTC | Move red1_eq_term_upto_univ_l to Equality | 07 July 2019, 19:17:39 UTC |
| 6ff71f5 | Théo Winterhalter | 07 July 2019, 14:49:32 UTC | Finally prove red1_eq_term_upto_univ_l | 07 July 2019, 14:49:32 UTC |
| a1bfac4 | Théo Winterhalter | 07 July 2019, 14:30:26 UTC | Add OnOne2_impl_exist_and_All as a new attempt | 07 July 2019, 14:30:26 UTC |
| c00f20a | Théo Winterhalter | 07 July 2019, 14:02:47 UTC | Another attempt at red1_eq_term before moving to OnOne2_indl again | 07 July 2019, 14:02:47 UTC |
| 01c164c | Théo Winterhalter | 07 July 2019, 13:21:11 UTC | Still not there for red1_eq_term | 07 July 2019, 13:21:11 UTC |
| 3b08fa9 | Théo Winterhalter | 07 July 2019, 13:09:08 UTC | One more step of red1_eq_term | 07 July 2019, 13:09:08 UTC |
| 103e4f9 | Théo Winterhalter | 07 July 2019, 12:49:07 UTC | Progress with red1_eq_term_upto_univ_l | 07 July 2019, 12:49:07 UTC |
| 4e97fa9 | Théo Winterhalter | 06 July 2019, 22:31:47 UTC | Try to prove red1_eq_term_upto_univ_l It's not as easy as the other one. | 06 July 2019, 22:31:47 UTC |
| b955d35 | Théo Winterhalter | 06 July 2019, 20:42:59 UTC | Merge pull request #197 from yforster/new-erasure Implementation of erasure | 06 July 2019, 20:42:59 UTC |
| 22d6b3e | Yannick Forster | 06 July 2019, 20:15:55 UTC | Fix compilation | 06 July 2019, 20:15:55 UTC |
| e88c04e | Yannick Forster | 06 July 2019, 19:50:10 UTC | One more admit closed | 06 July 2019, 19:57:23 UTC |
| 848b03c | Yannick Forster | 06 July 2019, 18:01:49 UTC | fix compilation | 06 July 2019, 19:57:23 UTC |
| 008d109 | Yannick Forster | 06 July 2019, 15:31:42 UTC | Annotation for admits | 06 July 2019, 19:57:23 UTC |
| 397d95e | Yannick Forster | 06 July 2019, 15:22:27 UTC | cleanup | 06 July 2019, 19:57:23 UTC |
| a1b74ce | Yannick Forster | 06 July 2019, 15:12:18 UTC | Refactored a lot, most files are admit free, apart from EArities | 06 July 2019, 19:57:23 UTC |
| e9b1ad1 | Yannick Forster | 06 July 2019, 10:53:32 UTC | Closed main proofs, missing auxiliary stuff + termination of is_arity | 06 July 2019, 19:57:23 UTC |
| be36603 | Yannick Forster | 06 July 2019, 10:36:59 UTC | add assumption on Prop <= Type | 06 July 2019, 19:57:23 UTC |
| 272b476 | Yannick Forster | 06 July 2019, 10:09:29 UTC | Progress using inversions | 06 July 2019, 19:57:23 UTC |
| e06c594 | Yannick Forster | 06 July 2019, 10:09:21 UTC | Make merge compile | 06 July 2019, 19:57:23 UTC |
| 1770dfd | Yannick Forster | 06 July 2019, 07:26:33 UTC | Progress | 06 July 2019, 19:55:13 UTC |
| c603634 | Yannick Forster | 05 July 2019, 20:49:08 UTC | Progress | 06 July 2019, 19:55:13 UTC |
| e494db0 | Yannick Forster | 05 July 2019, 09:19:06 UTC | Cleanup | 06 July 2019, 19:55:13 UTC |
| aeb6baa | Yannick Forster | 05 July 2019, 08:47:45 UTC | axiomatise checker only | 06 July 2019, 19:55:13 UTC |
| 9925af9 | Yannick Forster | 05 July 2019, 08:34:25 UTC | Added new extraction files | 06 July 2019, 19:55:13 UTC |
| 30ef5a5 | Matthieu Sozeau | 06 July 2019, 17:59:07 UTC | Merge pull request #196 from MetaCoq/principality Principality | 06 July 2019, 17:59:07 UTC |
| cd7e68b | Théo Winterhalter | 06 July 2019, 16:51:24 UTC | Refactoring to place red1_eq_context_upto_l in the right place | 06 July 2019, 17:38:59 UTC |
| 89be771 | Théo Winterhalter | 06 July 2019, 16:33:11 UTC | Prove red1_eq_context_upto_l | 06 July 2019, 16:33:11 UTC |
| adf7b34 | Théo Winterhalter | 06 July 2019, 16:28:42 UTC | Success with OnOne2_ind_l! | 06 July 2019, 16:28:42 UTC |
| d63bbd1 | Théo Winterhalter | 06 July 2019, 16:15:25 UTC | New attempt with OnOne2 | 06 July 2019, 16:15:25 UTC |
| 7b17869 | Théo Winterhalter | 06 July 2019, 13:12:53 UTC | Try to provide a new induction principle on OnOne2 but fail to use it | 06 July 2019, 13:12:53 UTC |
| 428aaf9 | Théo Winterhalter | 06 July 2019, 11:28:18 UTC | Use term_forall_list_rec for principality | 06 July 2019, 11:28:18 UTC |
| c5ffd97 | Théo Winterhalter | 06 July 2019, 11:19:53 UTC | Fix compilation by importing Principality | 06 July 2019, 11:19:53 UTC |
| 0a9ced1 | Théo Winterhalter | 06 July 2019, 11:15:44 UTC | cumul_confluence is probably not the right lemma | 06 July 2019, 11:15:44 UTC |
| 97b915c | Théo Winterhalter | 06 July 2019, 11:11:12 UTC | Add missing Derive | 06 July 2019, 11:11:12 UTC |
| 4a4085c | Matthieu Sozeau | 06 July 2019, 06:15:42 UTC | Proven a lot of the principality cases. | 06 July 2019, 06:15:42 UTC |
| 5ff32e9 | Matthieu Sozeau | 06 July 2019, 02:02:34 UTC | WIP on principality | 06 July 2019, 02:03:06 UTC |
| ebd608c | Théo Winterhalter | 05 July 2019, 21:57:25 UTC | Merge pull request #195 from yforster/extend-utils More lemmas for utils | 05 July 2019, 21:57:25 UTC |
| 8bb2466 | Matthieu Sozeau | 05 July 2019, 21:30:10 UTC | Completing the proof of validity. (#177) * WIP fixing validity proof * Move eq_term_upto_univ to Type, fix and simplify proofs * WIP fixing validity proof Lots of additional lemmas on context_subst/subslet needed. Not being paranoid in the typing relation renders this a bit harder than strictly necessary. | 05 July 2019, 21:30:10 UTC |
| 8f0836a | Yannick Forster | 05 July 2019, 21:00:14 UTC | fix compilation | 05 July 2019, 21:00:14 UTC |
| c2ba01b | Yannick Forster | 05 July 2019, 20:58:49 UTC | more utils lemmas | 05 July 2019, 20:58:49 UTC |
| 89bc1fd | Yannick Forster | 05 July 2019, 20:51:05 UTC | re-add DestArity | 05 July 2019, 20:51:05 UTC |
| 748c2c6 | Yannick Forster | 05 July 2019, 08:31:51 UTC | Fix compilation | 05 July 2019, 20:49:37 UTC |
| 723968a | Yannick Forster | 05 July 2019, 08:14:23 UTC | Some more auxiliary lemmas | 05 July 2019, 20:49:37 UTC |
| 135db3f | SimonBoulier | 05 July 2019, 16:47:06 UTC | Starting fixing the proofs of TemplateCoq | 05 July 2019, 16:49:27 UTC |
| 04458be | SimonBoulier | 05 July 2019, 16:46:53 UTC | Continuing a bit PCUICTyping (without being able to compile) | 05 July 2019, 16:48:56 UTC |
