| 2d631dc | Meven | 03 February 2021, 23:41:40 UTC | adapting the README | 03 February 2021, 23:45:57 UTC |
| fa5482b | Meven | 03 February 2021, 18:55:18 UTC | more cleaning up | 03 February 2021, 23:39:29 UTC |
| d9c634b | Meven | 03 February 2021, 23:39:18 UTC | principality | 03 February 2021, 23:39:18 UTC |
| 5e4986e | Meven | 03 February 2021, 23:16:01 UTC | moving todo | 03 February 2021, 23:16:01 UTC |
| 47fd39e | Meven | 03 February 2021, 23:14:31 UTC | uniqueness | 03 February 2021, 23:14:31 UTC |
| a9b4d81 | Meven | 03 February 2021, 18:55:31 UTC | starting uniqueness | 03 February 2021, 18:55:31 UTC |
| 6de3e5c | Meven | 03 February 2021, 18:55:18 UTC | more cleaning up | 03 February 2021, 18:55:18 UTC |
| edca4b8 | Meven | 03 February 2021, 10:30:23 UTC | removing last admit | 03 February 2021, 10:30:23 UTC |
| f505da6 | Meven | 02 February 2021, 13:32:26 UTC | cleaning up | 03 February 2021, 08:25:01 UTC |
| d9ee37e | Meven | 02 February 2021, 11:48:49 UTC | singling out the last lemma | 03 February 2021, 08:25:01 UTC |
| 074709a | Meven | 01 February 2021, 13:28:32 UTC | proving type_local_ctx_impl | 03 February 2021, 08:25:01 UTC |
| 775bbfd | Meven | 31 January 2021, 16:46:22 UTC | check on params -> type on params | 03 February 2021, 08:25:01 UTC |
| b8f8ef4 | Meven | 31 January 2021, 14:16:44 UTC | removing admits from BDFromPCUIC | 03 February 2021, 08:25:01 UTC |
| cda52a3 | Meven | 31 January 2021, 12:50:41 UTC | reducing ctx_inst holes | 03 February 2021, 08:25:01 UTC |
| 0af642a | Meven | 29 January 2021, 18:16:35 UTC | leaving only one typing hole | 03 February 2021, 08:25:01 UTC |
| 72aec12 | Meven | 28 January 2021, 15:04:55 UTC | updating build_branches_type_wt | 03 February 2021, 08:25:01 UTC |
| 25668dc | Meven | 27 January 2021, 17:22:16 UTC | filling up holes | 03 February 2021, 08:25:01 UTC |
| 2c8c51a | Meven | 27 January 2021, 13:45:35 UTC | missing two small holes in BDToPCUIC | 03 February 2021, 08:25:01 UTC |
| a91c49c | Meven | 27 January 2021, 09:17:57 UTC | updated typing | 03 February 2021, 08:25:01 UTC |
| 26c74ec | Meven | 26 January 2021, 18:32:31 UTC | updated readme | 03 February 2021, 08:25:01 UTC |
| e0c9776 | Meven | 26 January 2021, 18:20:53 UTC | cleaning up | 03 February 2021, 08:25:01 UTC |
| 0054f59 | Meven | 26 January 2021, 08:07:07 UTC | ongoing stuff | 03 February 2021, 08:25:01 UTC |
| 98c3ae8 | Meven | 03 December 2020, 16:15:21 UTC | PCUICToBD with a fixed global env | 03 February 2021, 08:25:01 UTC |
| 63a26f3 | Meven | 03 December 2020, 16:09:12 UTC | moving BDTyping and BDToPCUIC to fixed global env | 03 February 2021, 08:25:01 UTC |
| ab98f46 | Meven | 03 December 2020, 13:26:15 UTC | removing bad stuff | 03 February 2021, 08:25:01 UTC |
| 2e4afd3 | Meven | 30 November 2020, 10:38:59 UTC | removed the extraneous type inference in the branches | 03 February 2021, 08:25:01 UTC |
| 4dcee08 | Meven | 20 November 2020, 14:35:33 UTC | fixpoint and projection | 03 February 2021, 08:25:01 UTC |
| 3646340 | Meven | 20 November 2020, 14:34:59 UTC | not all case branches infer the same type | 03 February 2021, 08:25:01 UTC |
| 03f373e | Meven | 20 November 2020, 09:03:39 UTC | undirected -> minimal, missing some cases | 03 February 2021, 08:25:01 UTC |
| c579cef | Meven | 18 November 2020, 22:38:39 UTC | minimal -> undirected | 03 February 2021, 08:25:01 UTC |
| 941fd14 | Meven | 18 November 2020, 15:24:11 UTC | minimal typing defined | 03 February 2021, 08:25:01 UTC |
| ebc27c0 | Meven | 18 November 2020, 11:12:19 UTC | making the searchable theorems clearer | 03 February 2021, 08:25:01 UTC |
| 4cc4139 | Meven | 18 November 2020, 10:51:29 UTC | cutting the loop in infering_sort | 03 February 2021, 08:25:01 UTC |
| 95c8cac | Meven | 18 November 2020, 10:15:15 UTC | more adaptation to global environment changes | 03 February 2021, 08:25:01 UTC |
| afe6642 | Meven | 17 November 2020, 16:48:09 UTC | adapted to MetaCoq changes – no more isWfArity | 03 February 2021, 08:25:01 UTC |
| 788242e | Meven | 17 November 2020, 15:10:27 UTC | removed unneeded dependancy | 03 February 2021, 08:25:01 UTC |
| 28b64b7 | Meven | 06 November 2020, 16:05:03 UTC | more paranoid bidirectional | 03 February 2021, 08:25:01 UTC |
| 9e9d1c0 | Meven | 05 November 2020, 15:09:23 UTC | added a bit of documentation | 03 February 2021, 08:25:01 UTC |
| c696dae | Meven | 03 November 2020, 16:39:36 UTC | bidirectional implies undirected | 03 February 2021, 08:25:01 UTC |
| ef0428e | Meven | 02 November 2020, 19:02:16 UTC | moved bidirectional typing towards paranoid | 03 February 2021, 08:25:01 UTC |
| e6ed0ed | Meven | 02 October 2020, 16:10:31 UTC | separating induction w/out contexts and induction w/ context | 03 February 2021, 08:25:01 UTC |
| 488184c | Meven | 30 September 2020, 15:23:21 UTC | minor | 03 February 2021, 08:25:01 UTC |
| 1c309be | Meven | 30 September 2020, 15:22:25 UTC | induction principle w/ admitted weakening | 03 February 2021, 08:25:01 UTC |
| efed27a | Meven | 30 September 2020, 14:56:25 UTC | type_local_ctx_impl | 03 February 2021, 08:25:01 UTC |
| a30e073 | Meven | 04 September 2020, 13:31:23 UTC | ignored CoqMakefile | 03 February 2021, 08:25:01 UTC |
| 9d2370d | Meven | 04 September 2020, 13:31:03 UTC | added All_local_env_rel | 03 February 2021, 08:25:01 UTC |
| b896760 | Meven | 04 September 2020, 10:02:41 UTC | Modified EnvironmentTyping to take sorting into account | 03 February 2021, 08:25:01 UTC |
| 8b40dfd | Meven | 04 September 2020, 09:49:32 UTC | CoqProject | 03 February 2021, 08:25:01 UTC |
| 836228f | Matthieu Sozeau | 02 February 2021, 21:28:19 UTC | Prove lemmas showing ctx_inst plays well with cumulativity of inductive types | 02 February 2021, 21:28:19 UTC |
| 6866edc | Matthieu Sozeau | 01 February 2021, 13:21:42 UTC | Add a lemma relating typing_spine and ctx_inst | 01 February 2021, 13:25:37 UTC |
| 19eae80 | Jakob Botsch Nielsen | 01 February 2021, 10:54:07 UTC | Update PCUICSafeLemmata, various refactorings | 01 February 2021, 10:54:07 UTC |
| f8ddf7c | Matthieu Sozeau | 29 January 2021, 20:45:37 UTC | Renaming of validity_term to validity | 29 January 2021, 21:13:39 UTC |
| cabe334 | Matthieu Sozeau | 29 January 2021, 14:01:57 UTC | Also include the (derivable) consistent_instance_ext hyp in cases for uniformity. | 29 January 2021, 15:32:39 UTC |
| 6151fe9 | Matthieu Sozeau | 29 January 2021, 02:30:35 UTC | Finished validity proof | 29 January 2021, 03:21:09 UTC |
| fc66073 | Matthieu Sozeau | 28 January 2021, 16:12:38 UTC | New ctx_inst hypothesis in Typing | 28 January 2021, 16:12:38 UTC |
| a3c3a5f | Jakob Botsch Nielsen | 28 January 2021, 10:22:49 UTC | Finish safe reduction | 28 January 2021, 10:24:42 UTC |
| 51ba714 | Matthieu Sozeau | 28 January 2021, 01:40:58 UTC | Finally everything compiles | 28 January 2021, 01:40:58 UTC |
| dfb9f4a | Matthieu Sozeau | 28 January 2021, 01:36:27 UTC | SafeChecker tests passing again | 28 January 2021, 01:36:27 UTC |
| f571a5e | Matthieu Sozeau | 28 January 2021, 01:29:47 UTC | Better printer for type-checking/conversion errors | 28 January 2021, 01:29:47 UTC |
| c34dbb8 | Matthieu Sozeau | 28 January 2021, 01:20:11 UTC | Params were substituted in the wrong order in case contexts too, fixed | 28 January 2021, 01:20:11 UTC |
| fdbb0c6 | Matthieu Sozeau | 28 January 2021, 00:16:16 UTC | Fix an order bug in iota_red! The arguments where substituted in the wrong order... | 28 January 2021, 00:16:16 UTC |
| ebde62a | Matthieu Sozeau | 27 January 2021, 22:38:00 UTC | A bug revealed by the safe checker, probably in reification | 27 January 2021, 22:38:00 UTC |
| 6f81b2c | Matthieu Sozeau | 27 January 2021, 22:13:17 UTC | Fix test-suite scripts | 27 January 2021, 22:13:17 UTC |
| ccecc44 | Matthieu Sozeau | 27 January 2021, 22:00:56 UTC | Fix the test-suite, and improve Pretty to print environments | 27 January 2021, 22:00:56 UTC |
| 16c25e5 | Matthieu Sozeau | 27 January 2021, 20:29:27 UTC | Add convenience constructors in AstUtils for building inductive and constructor bodies without redundant information | 27 January 2021, 20:29:27 UTC |
| 4a97025 | Matthieu Sozeau | 27 January 2021, 20:13:23 UTC | Adapted translations (todo in param_original, wrong on case and inductives) | 27 January 2021, 20:13:23 UTC |
| fcae1e0 | Matthieu Sozeau | 27 January 2021, 19:26:06 UTC | Add monad_utils as a dependency to the template monad plugin (useful to write partial functions) | 27 January 2021, 19:26:06 UTC |
| 22cfd3f | Matthieu Sozeau | 27 January 2021, 18:30:04 UTC | All plugins compile | 27 January 2021, 18:30:04 UTC |
| 309a3f5 | Matthieu Sozeau | 27 January 2021, 18:16:38 UTC | Add a utility function in AstUtils to go from the old representation of cases to the new one | 27 January 2021, 18:16:38 UTC |
| 675fbda | Matthieu Sozeau | 27 January 2021, 17:29:59 UTC | Remove spurious Locate command | 27 January 2021, 17:29:59 UTC |
| 3d5c348 | Matthieu Sozeau | 27 January 2021, 10:31:54 UTC | Update reification/quoting of inductives and cases | 27 January 2021, 17:28:10 UTC |
| ad72f4a | Matthieu Sozeau | 25 January 2021, 12:07:53 UTC | Remove unneeded file | 27 January 2021, 17:28:10 UTC |
| d684cce | Jakob Botsch Nielsen | 27 January 2021, 16:46:38 UTC | Update safe reduction soundness, still missing completeness | 27 January 2021, 16:46:38 UTC |
| 8beb451 | Jakob Botsch Nielsen | 26 January 2021, 16:41:42 UTC | Update PCUICConversion, PCUICNormal, PCUICConvCumInversion | 26 January 2021, 16:41:42 UTC |
| 744d46d | Matthieu Sozeau | 25 January 2021, 03:23:12 UTC | Updated erasure (with some todos) | 25 January 2021, 03:32:31 UTC |
| 3d8a8e8 | Matthieu Sozeau | 25 January 2021, 02:28:31 UTC | Finished with the checker | 25 January 2021, 02:28:31 UTC |
| 7821f3f | Matthieu Sozeau | 25 January 2021, 02:24:58 UTC | Finished updating safechecker (some todos left) | 25 January 2021, 02:24:58 UTC |
| 5d01f18 | Matthieu Sozeau | 24 January 2021, 19:48:52 UTC | Updated SafeConversion | 24 January 2021, 19:48:52 UTC |
| 2a0b944 | Matthieu Sozeau | 24 January 2021, 18:12:45 UTC | In Safe Retyping | 24 January 2021, 18:12:45 UTC |
| 63cca49 | Matthieu Sozeau | 24 January 2021, 15:15:43 UTC | Fix definitions of predicate/branch conversion | 24 January 2021, 15:15:43 UTC |
| 1811999 | Matthieu Sozeau | 24 January 2021, 10:49:12 UTC | Safe Reduce updated (with todos) | 24 January 2021, 10:49:12 UTC |
| 0d696d4 | Matthieu Sozeau | 24 January 2021, 00:47:37 UTC | Updated EqualityDec | 24 January 2021, 00:47:37 UTC |
| b5950b2 | Matthieu Sozeau | 24 January 2021, 00:47:18 UTC | Fix weird bug with make vos in WcbvEval | 24 January 2021, 00:47:18 UTC |
| c60a54f | Matthieu Sozeau | 24 January 2021, 00:36:34 UTC | Adapted EqualityDec | 24 January 2021, 00:36:34 UTC |
| b6bc547 | Matthieu Sozeau | 24 January 2021, 00:21:08 UTC | PCUICErrors updated | 24 January 2021, 00:21:08 UTC |
| 6c81863 | Matthieu Sozeau | 24 January 2021, 00:06:41 UTC | Updated WfReduction (no todos) | 24 January 2021, 00:06:41 UTC |
| ca6542e | Matthieu Sozeau | 23 January 2021, 23:49:38 UTC | Canonicity and ConvCumInversion (with some admits) | 23 January 2021, 23:49:38 UTC |
| 00147fa | Matthieu Sozeau | 23 January 2021, 23:30:36 UTC | Fixed elimination (little change in statements) | 23 January 2021, 23:30:36 UTC |
| 888f66b | Matthieu Sozeau | 23 January 2021, 22:34:47 UTC | Principality with todos (does not look too hard :) | 23 January 2021, 22:34:47 UTC |
| 5684127 | Matthieu Sozeau | 23 January 2021, 21:51:28 UTC | SN and cumulprop done (some todos left) | 23 January 2021, 22:07:15 UTC |
| fad7667 | Matthieu Sozeau | 23 January 2021, 21:12:49 UTC | Adapted SafeLemmatas, some todos on stacks left | 23 January 2021, 21:12:49 UTC |
| f7b4c00 | Matthieu Sozeau | 23 January 2021, 20:57:48 UTC | Adapted WcbvEval entirely | 23 January 2021, 20:57:48 UTC |
| d328f95 | Matthieu Sozeau | 23 January 2021, 20:30:08 UTC | Updated Alpha conversion proof. Could be derivable from nameless (or the other way around) | 23 January 2021, 20:30:08 UTC |
| 710919d | Matthieu Sozeau | 23 January 2021, 19:45:14 UTC | Adapted TemplateToPCUIC (most is todo, corrected statement of translation theorem though) | 23 January 2021, 20:01:47 UTC |
| b1c14d4 | Matthieu Sozeau | 23 January 2021, 18:19:19 UTC | Adapted SR (todos for Case) | 23 January 2021, 18:19:19 UTC |
| 801b5ad | Matthieu Sozeau | 23 January 2021, 15:52:45 UTC | Finished updating InductiveInversion! | 23 January 2021, 15:52:45 UTC |
| 3dae729 | Matthieu Sozeau | 23 January 2021, 12:53:22 UTC | WIP in InductiveInversion | 23 January 2021, 12:53:22 UTC |
| c805902 | Matthieu Sozeau | 22 January 2021, 20:34:32 UTC | Adapted Inductives (rather easily!) | 22 January 2021, 20:34:32 UTC |
| 45706c5 | Matthieu Sozeau | 22 January 2021, 17:29:43 UTC | TODOs | 22 January 2021, 17:29:43 UTC |
| 61b6bb8 | Matthieu Sozeau | 22 January 2021, 16:36:16 UTC | WIP renaming fold_context to fold_context_k | 22 January 2021, 17:02:59 UTC |
