| 6e8787b | SimonBoulier | 05 July 2019, 14:36:35 UTC | fix compilation | 05 July 2019, 14:36:35 UTC |
| 3200066 | SimonBoulier | 04 April 2019, 08:04:56 UTC | WIP Safe Checker | 05 July 2019, 13:51:22 UTC |
| d056e1a | SimonBoulier | 26 June 2019, 07:52:28 UTC | gitignore | 05 July 2019, 11:16:04 UTC |
| 1c5e5e9 | Théo Winterhalter | 04 July 2019, 18:14:27 UTC | Merge pull request #192 from TheoWinterhalter/liftsubst-rename-ok Liftsubst rename ok | 04 July 2019, 18:14:27 UTC |
| 366f661 | Théo Winterhalter | 04 July 2019, 15:57:54 UTC | Fix compilation | 04 July 2019, 16:46:45 UTC |
| faaadcb | Matthieu Sozeau | 04 July 2019, 05:42:28 UTC | Fix admitted lemma with wrong assumption (missing an equality check on annotations) | 04 July 2019, 05:42:28 UTC |
| 93fa065 | Matthieu Sozeau | 04 July 2019, 05:33:57 UTC | Finished confluence: only remaining admits are in PCUICReduction: congruence for red | 04 July 2019, 05:36:48 UTC |
| 8ecaae7 | Matthieu Sozeau | 04 July 2019, 01:47:46 UTC | pred1_red1 can actually choose the left or right context | 04 July 2019, 01:47:46 UTC |
| aabcf5f | Matthieu Sozeau | 03 July 2019, 23:26:00 UTC | Finish proof of confluence for red1 without context fixing. | 03 July 2019, 23:26:18 UTC |
| 3132183 | Théo Winterhalter | 03 July 2019, 11:44:06 UTC | Add allow_cofix and prop_sub_type flags (#190) | 03 July 2019, 11:44:06 UTC |
| 57c0e40 | Matthieu Sozeau | 02 July 2019, 20:12:08 UTC | Finish proof of red -> pred1 using a kind of pred1 context conversion lemma. Separated the derived facts from parallel reduction confluence from reduction confluence. | 02 July 2019, 20:14:18 UTC |
| f1e61d3 | Matthieu Sozeau | 02 July 2019, 16:30:22 UTC | Move Confluence to ParallelReductionConfluence | 02 July 2019, 16:31:00 UTC |
| b037b12 | Théo Winterhalter | 02 July 2019, 14:47:46 UTC | Merge pull request #189 from TheoWinterhalter/squash-wf Squash wf in reduction and conversion so that it gets erased | 02 July 2019, 14:47:46 UTC |
| 93114bd | Théo Winterhalter | 02 July 2019, 12:23:38 UTC | Squash wf so that it gets erased | 02 July 2019, 12:53:06 UTC |
| 4ea7801 | Matthieu Sozeau | 02 July 2019, 02:30:10 UTC | Rebased on coq-8.8 | 02 July 2019, 02:35:24 UTC |
| a074105 | Matthieu Sozeau | 02 July 2019, 02:00:34 UTC | Updated everything to a new `unfold_fix` definition that requires fix bodies to be lambdas This is true of well-typed terms, and actually necessary to prove confluence! | 02 July 2019, 02:06:59 UTC |
| 45c5fcc | Matthieu Sozeau | 01 July 2019, 22:39:32 UTC | Confluence finished, finally! Fixpoints were real tricky! | 02 July 2019, 02:05:32 UTC |
| 6d65065 | Matthieu Sozeau | 30 June 2019, 22:50:33 UTC | Finished cofix/constructor reduction, rho_rename is proven | 02 July 2019, 02:05:32 UTC |
| 400849d | Matthieu Sozeau | 30 June 2019, 20:55:40 UTC | Finished Fix/Beta critical pair! | 02 July 2019, 02:05:32 UTC |
| d4e00ad | Matthieu Sozeau | 28 June 2019, 23:35:37 UTC | Yay, proven simplification lemma for app redexes, only remaining a good way to apply it. | 02 July 2019, 02:05:32 UTC |
| e14911b | Matthieu Sozeau | 28 June 2019, 04:17:58 UTC | Cleanup, make it compile. Only well-formedness hypotheses to finish | 02 July 2019, 02:05:32 UTC |
| 3df4bb8 | Matthieu Sozeau | 27 June 2019, 21:33:52 UTC | WIP finishing rho_rename: difficult because of the critical pairs due to n-ary fixpoints and co | 02 July 2019, 02:04:46 UTC |
| 11c5fce | Matthieu Sozeau | 27 June 2019, 07:15:33 UTC | Checked the rho_rename can be proven, cleanup a little bit | 02 July 2019, 02:04:46 UTC |
| 2d2cf01 | Matthieu Sozeau | 27 June 2019, 06:46:46 UTC | Strong substitutivity proven. Dealing with fixpoints almost finished Remains to finish the rho_rename proof too, otherwise, we have confluence! | 02 July 2019, 02:03:22 UTC |
| 2867d41 | Matthieu Sozeau | 26 June 2019, 23:22:47 UTC | Strong substitutivity proven up two delta and proj-cofix cases! | 02 July 2019, 02:03:22 UTC |
| 93971df | Matthieu Sozeau | 25 June 2019, 00:12:23 UTC | WIP proving strong substitutivity of parallel reduction | 02 July 2019, 02:03:22 UTC |
| d7a5e9b | Matthieu Sozeau | 22 June 2019, 02:50:47 UTC | WIP stating and proving renaming property of rho for variables | 02 July 2019, 02:03:22 UTC |
| 553157e | Matthieu Sozeau | 28 May 2019, 09:40:11 UTC | WIP improving notations/reasoning with \sigma-calculus, and proving confluence | 02 July 2019, 02:03:22 UTC |
| 54e05fe | Matthieu Sozeau | 26 May 2019, 14:33:27 UTC | Rename [cons/consn] to [subst_cons/consn] to avoid conflict with list [cons] | 02 July 2019, 02:03:22 UTC |
| 39e0c62 | Matthieu Sozeau | 26 May 2019, 14:28:43 UTC | Fix compilation | 02 July 2019, 02:03:22 UTC |
| 8393a21 | Matthieu Sozeau | 25 May 2019, 15:58:43 UTC | Proving all \sigma-calculus equations for `inst` version of substitution | 02 July 2019, 02:03:22 UTC |
| 2111aef | Matthieu Sozeau | 24 May 2019, 18:11:08 UTC | Show that lift/subst can also be implemented using renamings and instantiations. Idea suggested by Y. Forster. This brings \sigma-calculus primitives in, with which we can hopefully prove the lifting property of the rho function in PCUICConfluence more easily. Due to the `nat -> nat`/`nat -> term` encoding of renamings/substitutions in this presentation, we will however need to prove boring extensionality lemmas. | 02 July 2019, 02:03:22 UTC |
| cfcd181 | Matthieu Sozeau | 02 July 2019, 02:00:02 UTC | Merge pull request #188 from TheoWinterhalter/use-flags Make PCUICCumulativity generic in checker_flags | 02 July 2019, 02:00:02 UTC |
| fff27dc | Matthieu Sozeau | 01 July 2019, 19:46:44 UTC | Merge pull request #187 from TheoWinterhalter/let-lemmata Let lemmata | 01 July 2019, 19:46:44 UTC |
| ff81734 | Matthieu Sozeau | 01 July 2019, 19:04:18 UTC | Merge pull request #186 from TheoWinterhalter/fix-let Update wf_local to match LetIn | 01 July 2019, 19:04:18 UTC |
| b4a0e33 | Théo Winterhalter | 30 June 2019, 17:24:13 UTC | Make PCUICCumulativity generic in checker_flags | 30 June 2019, 17:25:17 UTC |
| 66f156f | Théo Winterhalter | 30 June 2019, 17:07:29 UTC | Prove inversion_it_mkLambda_or_LetIn Modulo checker_flags general cumulativity lemmata | 30 June 2019, 17:07:48 UTC |
| 7cbd105 | Théo Winterhalter | 30 June 2019, 17:07:02 UTC | Prove cumul_it_mkProd_or_LetIn | 30 June 2019, 17:07:48 UTC |
| 15083ba | Théo Winterhalter | 30 June 2019, 16:39:15 UTC | Derive it_mkLambda_or_LetIn_welltyped instead of proving it from scratch | 30 June 2019, 16:39:15 UTC |
| 66ad56a | Théo Winterhalter | 30 June 2019, 16:20:30 UTC | Move type_it_mkLambda_or_LetIn in PCUICGeneration Is it the right place? | 30 June 2019, 16:33:55 UTC |
| 33d74a3 | Théo Winterhalter | 29 June 2019, 18:54:03 UTC | Now prove typing lemmata for it_mkLambda_or_LetIn | 29 June 2019, 18:54:03 UTC |
| 6528d2d | Théo Winterhalter | 29 June 2019, 18:28:45 UTC | Update PCUICSR to new wf_local | 29 June 2019, 18:28:45 UTC |
| 496a726 | Théo Winterhalter | 29 June 2019, 18:17:16 UTC | Update PCUICConfluence to new wf_local | 29 June 2019, 18:24:40 UTC |
| d7994c5 | Théo Winterhalter | 29 June 2019, 18:13:16 UTC | Update PCUICParallelReduction to new wf_local | 29 June 2019, 18:13:16 UTC |
| 1747402 | Théo Winterhalter | 29 June 2019, 18:03:55 UTC | Update PCUICValidity to new wf_local | 29 June 2019, 18:03:55 UTC |
| af3b75c | Théo Winterhalter | 29 June 2019, 17:50:52 UTC | Update TemplateToPUICCorrectness to new wf_local | 29 June 2019, 17:50:52 UTC |
| 561a241 | Théo Winterhalter | 29 June 2019, 17:45:54 UTC | Update PCUICSubstitution with new wf_local | 29 June 2019, 17:45:58 UTC |
| 41c8bd0 | Théo Winterhalter | 29 June 2019, 17:18:44 UTC | Update WeakeningEnv with new wf_local | 29 June 2019, 17:18:44 UTC |
| c44df48 | Théo Winterhalter | 29 June 2019, 16:55:19 UTC | Update WeakeningEnv with new wf_local | 29 June 2019, 16:55:19 UTC |
| 5ce9648 | Théo Winterhalter | 29 June 2019, 16:28:43 UTC | Update PCUICTyping with new wf_local | 29 June 2019, 16:47:39 UTC |
| a39bc02 | Théo Winterhalter | 29 June 2019, 07:12:15 UTC | Update Substitution with new wf_local | 29 June 2019, 07:24:15 UTC |
| d06d386 | Théo Winterhalter | 29 June 2019, 03:03:30 UTC | Update Weakening with new wf_local | 29 June 2019, 06:47:44 UTC |
| 1e0a7fc | Théo Winterhalter | 28 June 2019, 22:37:16 UTC | Fix typing_all_wf_decl | 28 June 2019, 22:37:16 UTC |
| 3f9754f | Théo Winterhalter | 28 June 2019, 22:28:01 UTC | Odd proof of All_local_env_wf_decl | 28 June 2019, 22:28:01 UTC |
| bc4296e | Théo Winterhalter | 28 June 2019, 22:18:54 UTC | Fix typing_ind_env | 28 June 2019, 22:18:54 UTC |
| 47d43a6 | Théo Winterhalter | 28 June 2019, 22:15:00 UTC | Update wf_local_inv | 28 June 2019, 22:15:00 UTC |
| 0d3ec26 | Théo Winterhalter | 28 June 2019, 21:10:16 UTC | [WIP] Update wf_local to match LetIn | 28 June 2019, 21:44:48 UTC |
| e0a5dc1 | Théo Winterhalter | 28 June 2019, 21:02:29 UTC | Merge pull request #185 from TheoWinterhalter/coq-8.8 Move mkApps properties to their rightful place | 28 June 2019, 21:02:29 UTC |
| 7821bea | Théo Winterhalter | 28 June 2019, 19:21:46 UTC | Move mkApps properties to their rightful place | 28 June 2019, 19:33:26 UTC |
| a882427 | Matthieu Sozeau | 28 June 2019, 18:58:55 UTC | Merge pull request #184 from TheoWinterhalter/cumul-lambda Add cumulativity for λ-abstractions' bodies | 28 June 2019, 18:58:55 UTC |
| 84f5e07 | Théo Winterhalter | 28 June 2019, 18:24:01 UTC | Complete proof of cumul_zippx | 28 June 2019, 18:24:01 UTC |
| 531a8ab | Théo Winterhalter | 28 June 2019, 18:14:24 UTC | Merge pull request #183 from TheoWinterhalter/cumul-proofs Cumulativity / conversion proofs and refactoring | 28 June 2019, 18:14:24 UTC |
| 40c87bc | Théo Winterhalter | 28 June 2019, 18:11:47 UTC | Prove cumul_it_mkLambda_or_LetIn | 28 June 2019, 18:11:47 UTC |
| b365f44 | Théo Winterhalter | 28 June 2019, 17:55:39 UTC | Use cumulativity on body of λs | 28 June 2019, 18:07:11 UTC |
| 83a4472 | Théo Winterhalter | 28 June 2019, 17:48:02 UTC | Start proving cumul_it_mkLambda_or_LetIn but need cumul for lambda | 28 June 2019, 17:48:02 UTC |
| 7a29289 | Théo Winterhalter | 28 June 2019, 17:19:32 UTC | Moving cumulativity lemmata in PCUICCumulativity | 28 June 2019, 17:23:45 UTC |
| fb21035 | Théo Winterhalter | 28 June 2019, 17:01:26 UTC | More conversions, fix and prove conv_context | 28 June 2019, 17:01:34 UTC |
| 77a19ed | Matthieu Sozeau | 28 June 2019, 14:23:13 UTC | Merge pull request #181 from TheoWinterhalter/more-proofs Transitivity of `eq_term` and co | 28 June 2019, 14:23:13 UTC |
| e1856f0 | Théo Winterhalter | 28 June 2019, 00:17:17 UTC | Dealing with a lot of cumul/conv lemmata | 28 June 2019, 00:24:04 UTC |
| 96c2138 | Théo Winterhalter | 27 June 2019, 21:57:20 UTC | Move eq_trans to PCUICEquality | 27 June 2019, 21:57:20 UTC |
| 373dde9 | Théo Winterhalter | 27 June 2019, 21:48:18 UTC | Prove (l)eq_term_trans | 27 June 2019, 21:48:58 UTC |
| 3f4d139 | Théo Winterhalter | 27 June 2019, 21:37:59 UTC | Prove transitivity of (l)eq_universe | 27 June 2019, 21:37:59 UTC |
| 4a2edee | Théo Winterhalter | 27 June 2019, 21:29:25 UTC | Prove eq_term_upto_univ_trans | 27 June 2019, 21:29:25 UTC |
| 45dcc57 | Théo Winterhalter | 27 June 2019, 19:07:02 UTC | Almost prove red1_eq_context_upto_l, fix_context problem | 27 June 2019, 19:07:02 UTC |
| 42f31ee | Théo Winterhalter | 27 June 2019, 18:00:31 UTC | Start proving red1_eq_context_upto_l | 27 June 2019, 18:07:33 UTC |
| 551e4e4 | Matthieu Sozeau | 27 June 2019, 16:53:16 UTC | Merge pull request #179 from TheoWinterhalter/coq-8.8 Fix some lemmata | 27 June 2019, 16:53:16 UTC |
| 66f8137 | Théo Winterhalter | 27 June 2019, 16:39:03 UTC | Move some lemmata to SafeLemmata | 27 June 2019, 16:42:47 UTC |
| 54b8a52 | Théo Winterhalter | 27 June 2019, 16:31:22 UTC | Cleaning | 27 June 2019, 16:31:22 UTC |
| 6859016 | Théo Winterhalter | 27 June 2019, 16:26:08 UTC | Update eq_term_upto_univ_subst_instance_constr with new universes | 27 June 2019, 16:26:08 UTC |
| f5f47ef | Théo Winterhalter | 27 June 2019, 16:08:06 UTC | Merge remote-tracking branch 'Template-Coq/coq-8.8' into coq-8.8 | 27 June 2019, 16:08:06 UTC |
| 379fe11 | SimonBoulier | 13 May 2019, 07:27:28 UTC | implem universes graph | 27 June 2019, 07:12:35 UTC |
| d42f2e8 | Théo Winterhalter | 27 June 2019, 05:56:23 UTC | Move Forall2 lemmata | 27 June 2019, 05:56:23 UTC |
| 1d672be | Théo Winterhalter | 27 June 2019, 04:45:33 UTC | Move eq_term_upto_univ_substs to Equality | 27 June 2019, 04:45:33 UTC |
| 52f0a33 | Théo Winterhalter | 27 June 2019, 04:29:53 UTC | Complete proof of eq_term_upto_univ_substs | 27 June 2019, 04:29:53 UTC |
| cac3ad5 | Théo Winterhalter | 27 June 2019, 03:56:08 UTC | Define SubstUnivPreserving to shorten statements | 27 June 2019, 03:56:08 UTC |
| b610ac5 | Théo Winterhalter | 27 June 2019, 03:37:04 UTC | Move eq_context in PCUICEquality | 27 June 2019, 03:37:04 UTC |
| 946f7e9 | Théo Winterhalter | 26 June 2019, 21:40:24 UTC | Add Forall2_rev and a weak Forall2_mapi | 26 June 2019, 21:40:24 UTC |
| e213fba | Théo Winterhalter | 26 June 2019, 19:13:38 UTC | Add Forall2_eq_context_upto | 26 June 2019, 19:13:38 UTC |
| 75ffb7f | Théo Winterhalter | 26 June 2019, 18:52:51 UTC | New eq_context lemmata | 26 June 2019, 18:54:07 UTC |
| e12ed81 | Théo Winterhalter | 26 June 2019, 17:22:26 UTC | Almost complete red1_eq_term_upto_univ_l | 26 June 2019, 17:22:26 UTC |
| c840f55 | Théo Winterhalter | 26 June 2019, 16:21:07 UTC | Remove no longer used cheat axiom | 26 June 2019, 16:21:07 UTC |
| fa8ec4f | Théo Winterhalter | 26 June 2019, 01:47:18 UTC | Minor progress | 26 June 2019, 01:47:18 UTC |
| 17ba4e7 | Théo Winterhalter | 26 June 2019, 00:18:53 UTC | Fix cored_eq_term_upto_univ_r | 26 June 2019, 00:18:53 UTC |
| 9c9bc82 | Théo Winterhalter | 25 June 2019, 23:38:02 UTC | Progress with red1_eq_term_upto_univ_l | 25 June 2019, 23:38:02 UTC |
| d56b61a | Théo Winterhalter | 25 June 2019, 19:20:40 UTC | Add eq_context_upto relation | 25 June 2019, 19:20:40 UTC |
| c8f7d29 | Théo Winterhalter | 25 June 2019, 17:22:09 UTC | Complete all computation cases of red1_eq_term_upto_univ_l | 25 June 2019, 17:22:09 UTC |
| b9d8008 | Théo Winterhalter | 25 June 2019, 00:54:46 UTC | Weaken the lemma and progress | 25 June 2019, 00:54:46 UTC |
| c0bc039 | Théo Winterhalter | 25 June 2019, 00:26:48 UTC | Prove eq_term_upto_univ_subst_instance_constr assuming some irrelevance | 25 June 2019, 00:26:48 UTC |
| afed6ed | Théo Winterhalter | 24 June 2019, 23:31:34 UTC | First attempt at eq_term_upto_univ_subst_instance_constr | 24 June 2019, 23:31:34 UTC |
| 7f361ed | Théo Winterhalter | 24 June 2019, 22:59:33 UTC | Small progress with red1_eq_term_upto_univ_l | 24 June 2019, 22:59:33 UTC |
