| 2f220ef | Matthieu Sozeau | 22 January 2021, 16:21:20 UTC | Before renaming fold_context | 22 January 2021, 16:21:20 UTC |
| f8d1a0c | Matthieu Sozeau | 22 January 2021, 16:04:40 UTC | Remove unused PCUICtxShape | 22 January 2021, 16:12:13 UTC |
| 4bc6923 | Matthieu Sozeau | 22 January 2021, 15:51:02 UTC | TODOs in PCUICToTemplate | 22 January 2021, 15:51:02 UTC |
| 2f6fb43 | Matthieu Sozeau | 22 January 2021, 13:03:32 UTC | In inversion | 22 January 2021, 13:03:32 UTC |
| 60a73ed | Matthieu Sozeau | 22 January 2021, 12:39:46 UTC | Finished conversion (one todo left) | 22 January 2021, 12:39:46 UTC |
| 8ee93d4 | Matthieu Sozeau | 21 January 2021, 22:40:54 UTC | Fix definition of comparison of declarations | 22 January 2021, 10:42:15 UTC |
| e67b09a | Matthieu Sozeau | 21 January 2021, 21:04:24 UTC | Now in the safe zone :) Adapting conversion lemmas | 21 January 2021, 21:04:24 UTC |
| 692473a | Matthieu Sozeau | 21 January 2021, 19:49:56 UTC | Context Cumulativity/Conversion done | 21 January 2021, 19:49:56 UTC |
| 6426108 | Matthieu Sozeau | 21 January 2021, 18:19:06 UTC | WIP in Context Conversion | 21 January 2021, 18:19:06 UTC |
| 3be9be0 | Matthieu Sozeau | 21 January 2021, 14:12:27 UTC | Refine red type irrelevance: it preserves the step number | 21 January 2021, 14:12:27 UTC |
| 1ba2a31 | Matthieu Sozeau | 21 January 2021, 13:53:14 UTC | Finish confluence proofs (up to alpha-equivalence as well) | 21 January 2021, 13:53:14 UTC |
| b60ac24 | Matthieu Sozeau | 21 January 2021, 13:52:59 UTC | Refine RedTypeIrrelevance: only body reduction matters | 21 January 2021, 13:52:59 UTC |
| b16284a | Matthieu Sozeau | 21 January 2021, 03:53:38 UTC | Back in confluence with the right definitions | 21 January 2021, 03:53:38 UTC |
| 1484164 | Matthieu Sozeau | 21 January 2021, 02:52:55 UTC | Adapted confluence proof to new, correct context relation structure | 21 January 2021, 02:52:55 UTC |
| 1e33a4f | Matthieu Sozeau | 21 January 2021, 00:52:55 UTC | Factorize similar context relations into a general one | 21 January 2021, 02:16:08 UTC |
| 8c05bb7 | Matthieu Sozeau | 20 January 2021, 22:30:19 UTC | Before replacing All2_local_env | 20 January 2021, 22:30:19 UTC |
| dfc0c54 | Matthieu Sozeau | 20 January 2021, 21:08:19 UTC | Need to fix problem of name preservation missing from All2_local_env | 20 January 2021, 21:08:19 UTC |
| 967bd80 | Matthieu Sozeau | 20 January 2021, 20:51:52 UTC | Shown commnutation of eq_term and reduction | 20 January 2021, 20:51:52 UTC |
| f13b508 | Matthieu Sozeau | 20 January 2021, 14:13:20 UTC | Move eq_predicate Equivalence instances in separate lemmas | 20 January 2021, 14:13:20 UTC |
| 1771da3 | Matthieu Sozeau | 20 January 2021, 12:34:53 UTC | WIP in finishing confluence proof | 20 January 2021, 12:34:53 UTC |
| 87c754e | Matthieu Sozeau | 20 January 2021, 03:06:15 UTC | Finished updating confluence proof | 20 January 2021, 03:19:06 UTC |
| 12a894a | Matthieu Sozeau | 20 January 2021, 01:07:32 UTC | rho match case finished | 20 January 2021, 01:07:32 UTC |
| fd4193a | Matthieu Sozeau | 19 January 2021, 19:59:28 UTC | WIP in parallel reduction confluence | 19 January 2021, 19:59:28 UTC |
| 289abdb | Matthieu Sozeau | 19 January 2021, 02:13:41 UTC | Showing that rho_ctx is stable under renaming | 19 January 2021, 02:13:41 UTC |
| c6b25ea | Matthieu Sozeau | 18 January 2021, 15:57:58 UTC | WIP in confluence proof | 18 January 2021, 15:57:58 UTC |
| f9135de | Matthieu Sozeau | 17 January 2021, 22:25:01 UTC | WIP adapting rho function | 17 January 2021, 22:25:01 UTC |
| beae36c | Matthieu Sozeau | 17 January 2021, 21:32:18 UTC | Substitutivity of parallel reduction | 17 January 2021, 21:32:18 UTC |
| 1b8909d | Matthieu Sozeau | 17 January 2021, 13:04:31 UTC | WIP lifting parallel reduction to new case context reductions | 17 January 2021, 14:12:36 UTC |
| af59042 | Matthieu Sozeau | 17 January 2021, 12:25:35 UTC | Updated upto instantiation and normal | 17 January 2021, 12:25:35 UTC |
| a4f294a | Matthieu Sozeau | 17 January 2021, 11:43:34 UTC | Complete the theory of context reduction closure of red1 on one decl <-> context relation of reducing any term in the context | 17 January 2021, 11:43:34 UTC |
| 3474c64 | Matthieu Sozeau | 16 January 2021, 20:22:19 UTC | WIP in reduction is good | 16 January 2021, 20:22:19 UTC |
| 8d10ecc | Matthieu Sozeau | 16 January 2021, 18:51:04 UTC | Updating UnivSubstitution | 16 January 2021, 18:51:04 UTC |
| 94bab92 | Matthieu Sozeau | 15 January 2021, 21:02:29 UTC | WIP adapting Reduction to new reduction rules on contexts in cases | 16 January 2021, 11:52:14 UTC |
| 8dbf957 | Matthieu Sozeau | 15 January 2021, 17:50:44 UTC | Need a new reduction rule on contexts as expected | 15 January 2021, 17:50:44 UTC |
| 02827eb | Matthieu Sozeau | 15 January 2021, 11:42:33 UTC | Updated instantiation and substitution | 15 January 2021, 11:42:33 UTC |
| 1a304a5 | Matthieu Sozeau | 15 January 2021, 00:55:07 UTC | Adapted PCUICRename | 15 January 2021, 00:55:07 UTC |
| dd68d3c | Matthieu Sozeau | 14 January 2021, 19:33:14 UTC | Adapt PCUICUnivSubstitution | 14 January 2021, 19:33:14 UTC |
| 1173229 | Matthieu Sozeau | 14 January 2021, 18:01:36 UTC | Adapted OnFreeVars | 14 January 2021, 18:01:36 UTC |
| 5d44820 | Matthieu Sozeau | 14 January 2021, 11:11:36 UTC | Fully adapted PCUICNameless | 14 January 2021, 11:11:36 UTC |
| 0df06e7 | Matthieu Sozeau | 14 January 2021, 10:36:19 UTC | Updated Closed | 14 January 2021, 10:36:19 UTC |
| 51005a2 | Matthieu Sozeau | 14 January 2021, 08:58:17 UTC | WIP in PCUICClosed | 14 January 2021, 08:58:17 UTC |
| e358ebe | Matthieu Sozeau | 13 January 2021, 18:09:18 UTC | Adapted PCUICNormal | 13 January 2021, 18:09:18 UTC |
| e803b97 | Matthieu Sozeau | 13 January 2021, 17:40:09 UTC | Fix module includes to avoid growing rewrite databases for nothing | 13 January 2021, 17:40:09 UTC |
| c2be4d0 | Matthieu Sozeau | 13 January 2021, 17:01:26 UTC | Move EqDec instance for Ast.term away from Reflect, so as not to pollute PCUIC | 13 January 2021, 17:17:13 UTC |
| 7db4e9b | Matthieu Sozeau | 13 January 2021, 13:58:11 UTC | WeakeningEnv and Nameless updated | 13 January 2021, 13:58:11 UTC |
| dd0481f | Matthieu Sozeau | 13 January 2021, 10:22:54 UTC | Updated Typing to add new context conversion premisses | 13 January 2021, 10:24:19 UTC |
| cafa9de | Matthieu Sozeau | 12 January 2021, 20:57:31 UTC | WIP in simplifying reduction | 12 January 2021, 20:57:31 UTC |
| 13d4718 | Matthieu Sozeau | 12 January 2021, 20:38:26 UTC | Updated Equality | 12 January 2021, 20:38:26 UTC |
| 5cca998 | Matthieu Sozeau | 12 January 2021, 16:48:21 UTC | WIP in equality, now needing context equality | 12 January 2021, 16:48:21 UTC |
| 2fe7460 | Matthieu Sozeau | 12 January 2021, 16:00:08 UTC | Updated SigmaCalculus proofs | 12 January 2021, 16:00:08 UTC |
| dc07622 | Matthieu Sozeau | 11 January 2021, 18:47:06 UTC | Main infrastructure lemmas on contexts in cases proven | 11 January 2021, 18:47:06 UTC |
| f954b2c | Matthieu Sozeau | 11 January 2021, 16:03:25 UTC | Template <-> PCUIC translations defined | 11 January 2021, 16:03:25 UTC |
| a891b73 | Matthieu Sozeau | 09 January 2021, 14:46:21 UTC | Move to PCUIC having expanded contexts in Case nodes | 11 January 2021, 10:55:03 UTC |
| ec88526 | Matthieu Sozeau | 08 January 2021, 21:42:53 UTC | WIP | 08 January 2021, 21:42:53 UTC |
| fe9dfa2 | Matthieu Sozeau | 08 January 2021, 21:09:54 UTC | Try a simpler solution for pred allowing reflexivity on case | 08 January 2021, 21:09:54 UTC |
| bb61a04 | Matthieu Sozeau | 08 January 2021, 19:06:01 UTC | Updating Parallel Reduction to carry well-formedness predicates | 08 January 2021, 19:06:01 UTC |
| c2be5a1 | Matthieu Sozeau | 08 January 2021, 13:10:57 UTC | Finished substitution | 08 January 2021, 13:10:57 UTC |
| 3f6d0b8 | Matthieu Sozeau | 07 January 2021, 20:25:12 UTC | WIP in substitution lemmas | 07 January 2021, 20:25:12 UTC |
| 50190ca | Matthieu Sozeau | 07 January 2021, 19:51:21 UTC | Finished implementing substitution through instantiation. substitution lemma remains | 07 January 2021, 19:51:21 UTC |
| 9e58182 | Matthieu Sozeau | 07 January 2021, 16:51:58 UTC | Updated univ substitution | 07 January 2021, 16:51:58 UTC |
| 3da3351 | Matthieu Sozeau | 06 January 2021, 17:50:04 UTC | Half of universe instantiation done | 06 January 2021, 17:50:04 UTC |
| 43c13cc | Matthieu Sozeau | 06 January 2021, 16:16:38 UTC | Cleanup name of subst_instance lemmatas | 06 January 2021, 16:16:38 UTC |
| 24e6b2c | Matthieu Sozeau | 06 January 2021, 14:59:55 UTC | Use overloaded subst_instance in template-coq | 06 January 2021, 15:03:15 UTC |
| 6f8fdd9 | Matthieu Sozeau | 06 January 2021, 14:46:42 UTC | Before moving to overloaded subst_instance operation everywhere | 06 January 2021, 14:46:42 UTC |
| 81aa326 | Matthieu Sozeau | 06 January 2021, 11:55:36 UTC | Updating substitution and universe instantiation | 06 January 2021, 11:55:36 UTC |
| 1e119c6 | Matthieu Sozeau | 05 January 2021, 12:23:52 UTC | Finished instantiation proof | 05 January 2021, 12:23:52 UTC |
| 80c662c | Matthieu Sozeau | 05 January 2021, 12:15:50 UTC | Only eq_term upto instantiation remains | 05 January 2021, 12:15:50 UTC |
| eb7f0b4 | Matthieu Sozeau | 05 January 2021, 09:38:26 UTC | Only instantiation for cumulativity remaining | 05 January 2021, 09:38:26 UTC |
| 82c7d4e | Matthieu Sozeau | 04 January 2021, 22:20:40 UTC | WIP in instantiation theorem | 04 January 2021, 22:20:40 UTC |
| 2a53557 | Matthieu Sozeau | 04 January 2021, 12:47:01 UTC | Cleanup Weakening, move on_free_vars to a separate library | 04 January 2021, 12:47:01 UTC |
| 5dd9644 | Matthieu Sozeau | 28 December 2020, 14:44:29 UTC | Verified proof idea for strengthening (will have to come after subject reduction) | 28 December 2020, 14:44:29 UTC |
| d2df801 | Matthieu Sozeau | 28 December 2020, 03:19:03 UTC | Play with strengthening: not provable inductively as conversions can include arbitrary terms | 28 December 2020, 03:19:03 UTC |
| 537b9d3 | Matthieu Sozeau | 27 December 2020, 13:45:07 UTC | Proven renaming for shiftnP predicate | 27 December 2020, 13:45:07 UTC |
| 78881fd | Matthieu Sozeau | 27 December 2020, 03:39:26 UTC | Need to think about how to state the exchange lemma | 27 December 2020, 03:39:26 UTC |
| 2f37033 | Matthieu Sozeau | 27 December 2020, 02:43:35 UTC | Finished proof that reduction preserves free variables | 27 December 2020, 02:43:35 UTC |
| 8a5c296 | Matthieu Sozeau | 26 December 2020, 20:41:28 UTC | WIP on renaming proofs carrying variable information | 26 December 2020, 20:41:28 UTC |
| bc2366b | Matthieu Sozeau | 26 December 2020, 06:52:01 UTC | WIP finishing strengthening | 26 December 2020, 06:52:01 UTC |
| f7a3612 | Matthieu Sozeau | 26 December 2020, 06:03:40 UTC | Strenghten renaming theorem for exchange and strengthening. | 26 December 2020, 06:03:40 UTC |
| dc507c2 | Matthieu Sozeau | 24 December 2020, 15:19:56 UTC | Prove weakening... from instantiation | 24 December 2020, 16:26:43 UTC |
| d18eb24 | Matthieu Sozeau | 24 December 2020, 04:57:31 UTC | Completed renaming proof with new case. | 24 December 2020, 04:57:31 UTC |
| fbd5584 | Matthieu Sozeau | 24 December 2020, 01:26:31 UTC | Refactoring and proving renaming theorem | 24 December 2020, 01:26:31 UTC |
| 0a205ee | Matthieu Sozeau | 24 December 2020, 01:26:12 UTC | Better induction principle for "generated" contexts (fix/case/branches) | 24 December 2020, 01:26:12 UTC |
| 289b8b5 | Matthieu Sozeau | 23 December 2020, 19:04:15 UTC | SigmaCalculus is now self-contained and does not depend on Closed | 23 December 2020, 19:04:58 UTC |
| bd32ff3 | Matthieu Sozeau | 23 December 2020, 17:34:05 UTC | Big refactoring / cleanup of sigma calculus | 23 December 2020, 17:34:05 UTC |
| c294bd7 | Matthieu Sozeau | 23 December 2020, 15:22:51 UTC | Change declared_projection argument order | 23 December 2020, 15:23:06 UTC |
| ff845cc | Matthieu Sozeau | 23 December 2020, 15:14:39 UTC | Fic declared_constructor argument order | 23 December 2020, 15:14:39 UTC |
| 4f55189 | Matthieu Sozeau | 23 December 2020, 15:02:51 UTC | Switched arguments of declared_inductive | 23 December 2020, 15:02:51 UTC |
| 6714426 | Matthieu Sozeau | 23 December 2020, 14:47:49 UTC | Fix replace.sh | 23 December 2020, 14:47:49 UTC |
| 528de5b | Matthieu Sozeau | 23 December 2020, 14:22:37 UTC | Cleaning up sigma calculus proofs | 23 December 2020, 14:22:37 UTC |
| be5f608 | Matthieu Sozeau | 23 December 2020, 02:53:59 UTC | De bruijn bug in map_constructor_body... | 23 December 2020, 02:53:59 UTC |
| c61c55c | Matthieu Sozeau | 23 December 2020, 01:41:46 UTC | Almost complete nameless proof | 23 December 2020, 01:41:46 UTC |
| 676f1b2 | Matthieu Sozeau | 22 December 2020, 18:27:51 UTC | Cleanup PCUICClosed to use the right unfolding behaviors | 22 December 2020, 18:27:51 UTC |
| a9f14aa | Matthieu Sozeau | 22 December 2020, 13:52:33 UTC | WIP proviing renaming lemma | 22 December 2020, 13:52:33 UTC |
| 138ca1f | Matthieu Sozeau | 21 December 2020, 22:14:15 UTC | Now in sigmacalculus. Need to cleanup substitution/lifting lemmas for lets first. | 21 December 2020, 22:14:15 UTC |
| ebc9216 | Matthieu Sozeau | 21 December 2020, 17:36:25 UTC | Directly map on constructor list in case reduction | 21 December 2020, 17:36:25 UTC |
| 54ed6d4 | Matthieu Sozeau | 21 December 2020, 04:32:31 UTC | PCUICNormal working now | 21 December 2020, 04:32:31 UTC |
| e4aae53 | Matthieu Sozeau | 21 December 2020, 03:12:40 UTC | Updated upto PCUICTyping | 21 December 2020, 03:34:43 UTC |
| 7a73d53 | Matthieu Sozeau | 21 December 2020, 02:21:00 UTC | Done up to TypingWf | 21 December 2020, 02:21:00 UTC |
| 0f21b68 | Matthieu Sozeau | 21 December 2020, 01:33:06 UTC | WIP renaming | 21 December 2020, 01:33:06 UTC |
| a3d5866 | Matthieu Sozeau | 21 December 2020, 01:28:04 UTC | WIP with cleaned-up inductive and constructor representation | 21 December 2020, 01:28:04 UTC |
