| fef963e | Meven | 04 June 2021, 15:31:56 UTC | BDStrengthening, missing computation + the annoying cases | 04 June 2021, 15:31:56 UTC |
| ff0c9bb | Matthieu Sozeau | 03 May 2021, 14:56:36 UTC | Complete SR proof | 25 May 2021, 14:57:10 UTC |
| cec1284 | Matthieu Sozeau | 29 April 2021, 19:57:36 UTC | Progress in PCUICSR | 25 May 2021, 14:56:59 UTC |
| 4e15fd0 | Meven | 18 May 2021, 10:43:54 UTC | slight size simplification | 18 May 2021, 10:49:40 UTC |
| 42a51da | Meven | 11 March 2021, 14:33:31 UTC | updating wrt case-representation | 18 May 2021, 10:49:40 UTC |
| 7e900e0 | Meven | 12 February 2021, 15:45:01 UTC | moving bidirectional into pcuic | 18 May 2021, 10:46:31 UTC |
| c927906 | Meven | 11 February 2021, 15:47:58 UTC | adding BDUnique to the CoqProject | 18 May 2021, 10:46:31 UTC |
| b32a861 | Meven | 03 February 2021, 23:41:40 UTC | adapting the README | 18 May 2021, 10:46:31 UTC |
| 8706768 | Meven | 03 February 2021, 18:55:18 UTC | more cleaning up | 18 May 2021, 10:46:31 UTC |
| 48f4ffd | Meven | 03 February 2021, 23:39:18 UTC | principality | 18 May 2021, 10:46:31 UTC |
| 782d7e6 | Meven | 03 February 2021, 23:16:01 UTC | moving todo | 18 May 2021, 10:46:31 UTC |
| 52d617d | Meven | 03 February 2021, 23:14:31 UTC | uniqueness | 18 May 2021, 10:44:47 UTC |
| 1d826e5 | Meven | 03 February 2021, 18:55:31 UTC | starting uniqueness | 18 May 2021, 10:44:47 UTC |
| dded56a | Meven | 03 February 2021, 18:55:18 UTC | more cleaning up | 18 May 2021, 10:44:47 UTC |
| ef6f537 | Meven | 03 February 2021, 10:30:23 UTC | removing last admit | 18 May 2021, 10:44:47 UTC |
| 4acccae | Meven | 02 February 2021, 13:32:26 UTC | cleaning up | 18 May 2021, 10:44:47 UTC |
| caa0009 | Meven | 02 February 2021, 11:48:49 UTC | singling out the last lemma | 18 May 2021, 10:44:47 UTC |
| 4fa9669 | Meven | 01 February 2021, 13:28:32 UTC | proving type_local_ctx_impl | 18 May 2021, 10:44:47 UTC |
| 0ab9899 | Meven | 31 January 2021, 16:46:22 UTC | check on params -> type on params | 18 May 2021, 10:44:47 UTC |
| 7dd0c3e | Meven | 31 January 2021, 14:16:44 UTC | removing admits from BDFromPCUIC | 18 May 2021, 10:44:47 UTC |
| efdb5c7 | Meven | 31 January 2021, 12:50:41 UTC | reducing ctx_inst holes | 18 May 2021, 10:44:47 UTC |
| 4a1850a | Meven | 29 January 2021, 18:16:35 UTC | leaving only one typing hole | 18 May 2021, 10:44:47 UTC |
| 10878e7 | Meven | 28 January 2021, 15:04:55 UTC | updating build_branches_type_wt | 18 May 2021, 10:44:47 UTC |
| 071a0cb | Meven | 27 January 2021, 17:22:16 UTC | filling up holes | 18 May 2021, 10:44:47 UTC |
| 9f8dd18 | Meven | 27 January 2021, 13:45:35 UTC | missing two small holes in BDToPCUIC | 18 May 2021, 10:44:47 UTC |
| 22f6d5d | Meven | 27 January 2021, 09:17:57 UTC | updated typing | 18 May 2021, 10:44:47 UTC |
| a697e3f | Meven | 26 January 2021, 18:32:31 UTC | updated readme | 18 May 2021, 10:44:47 UTC |
| dbe3f92 | Meven | 26 January 2021, 18:20:53 UTC | cleaning up | 18 May 2021, 10:44:47 UTC |
| c277713 | Meven | 26 January 2021, 08:07:07 UTC | ongoing stuff | 18 May 2021, 10:44:47 UTC |
| 91bbcbe | Meven | 03 December 2020, 16:15:21 UTC | PCUICToBD with a fixed global env | 18 May 2021, 10:44:47 UTC |
| e8caadb | Meven | 03 December 2020, 16:09:12 UTC | moving BDTyping and BDToPCUIC to fixed global env | 18 May 2021, 10:44:47 UTC |
| a34f776 | Meven | 03 December 2020, 13:26:15 UTC | removing bad stuff | 18 May 2021, 10:44:47 UTC |
| bd39fd3 | Meven | 30 November 2020, 10:38:59 UTC | removed the extraneous type inference in the branches | 18 May 2021, 10:44:47 UTC |
| 103e05e | Meven | 20 November 2020, 14:35:33 UTC | fixpoint and projection | 18 May 2021, 10:44:47 UTC |
| c576a7a | Meven | 20 November 2020, 14:34:59 UTC | not all case branches infer the same type | 18 May 2021, 10:44:47 UTC |
| c9902d9 | Meven | 20 November 2020, 09:03:39 UTC | undirected -> minimal, missing some cases | 18 May 2021, 10:44:47 UTC |
| d98d0ba | Meven | 18 November 2020, 22:38:39 UTC | minimal -> undirected | 18 May 2021, 10:44:47 UTC |
| ec72f09 | Meven | 18 November 2020, 15:24:11 UTC | minimal typing defined | 18 May 2021, 10:44:47 UTC |
| 4d27f7d | Meven | 18 November 2020, 11:12:19 UTC | making the searchable theorems clearer | 18 May 2021, 10:44:47 UTC |
| 1ce5172 | Meven | 18 November 2020, 10:51:29 UTC | cutting the loop in infering_sort | 18 May 2021, 10:44:47 UTC |
| 8072b27 | Meven | 18 November 2020, 10:15:15 UTC | more adaptation to global environment changes | 18 May 2021, 10:44:47 UTC |
| 13353db | Meven | 17 November 2020, 16:48:09 UTC | adapted to MetaCoq changes – no more isWfArity | 18 May 2021, 10:44:47 UTC |
| d543624 | Meven | 17 November 2020, 15:10:27 UTC | removed unneeded dependancy | 18 May 2021, 10:44:47 UTC |
| 8880d9d | Meven | 06 November 2020, 16:05:03 UTC | more paranoid bidirectional | 18 May 2021, 10:44:47 UTC |
| e720ca7 | Meven | 05 November 2020, 15:09:23 UTC | added a bit of documentation | 18 May 2021, 10:44:47 UTC |
| 329da92 | Meven | 03 November 2020, 16:39:36 UTC | bidirectional implies undirected | 18 May 2021, 10:44:47 UTC |
| c3073ea | Meven | 02 November 2020, 19:02:16 UTC | moved bidirectional typing towards paranoid | 18 May 2021, 10:44:47 UTC |
| e902a46 | Meven | 02 October 2020, 16:10:31 UTC | separating induction w/out contexts and induction w/ context | 18 May 2021, 10:44:47 UTC |
| 35bad60 | Meven | 30 September 2020, 15:23:21 UTC | minor | 18 May 2021, 10:44:47 UTC |
| bd7ba83 | Meven | 30 September 2020, 15:22:25 UTC | induction principle w/ admitted weakening | 18 May 2021, 10:44:47 UTC |
| 001e9b9 | Meven | 30 September 2020, 14:56:25 UTC | type_local_ctx_impl | 18 May 2021, 10:44:47 UTC |
| ff25c15 | Meven | 04 September 2020, 13:31:23 UTC | ignored CoqMakefile | 18 May 2021, 10:44:47 UTC |
| 57a2698 | Meven | 04 September 2020, 13:31:03 UTC | added All_local_env_rel | 18 May 2021, 10:44:47 UTC |
| 903b7e1 | Meven | 04 September 2020, 10:02:41 UTC | Modified EnvironmentTyping to take sorting into account | 18 May 2021, 10:44:47 UTC |
| ca2afda | Meven | 04 September 2020, 09:49:32 UTC | CoqProject | 18 May 2021, 10:44:47 UTC |
| 0f7d22f | Matthieu Sozeau | 22 April 2021, 17:22:59 UTC | Progress in subject reduction, iota case closed | 22 April 2021, 17:22:59 UTC |
| a9163f5 | Matthieu Sozeau | 21 April 2021, 17:58:38 UTC | Progress in SR proof, at case | 21 April 2021, 17:58:38 UTC |
| b280775 | Matthieu Sozeau | 11 April 2021, 15:25:33 UTC | Fix implicits of `env_prop_*` | 11 April 2021, 15:25:33 UTC |
| fb06aac | Matthieu Sozeau | 10 April 2021, 16:47:43 UTC | Updated alpha-conversion proof, minor change in PCUICTyping | 10 April 2021, 16:47:43 UTC |
| e33ce67 | Matthieu Sozeau | 25 March 2021, 19:15:08 UTC | Some cleaning up | 30 March 2021, 00:33:55 UTC |
| 9bde3ae | Matthieu Sozeau | 25 March 2021, 16:57:22 UTC | Completed Inductive Inversion! | 25 March 2021, 16:57:22 UTC |
| 7af55a9 | Matthieu Sozeau | 24 March 2021, 23:55:33 UTC | Almost finished with Inductive Inversion: only an alpha-equivalence remains! | 24 March 2021, 23:55:33 UTC |
| 7795007 | Matthieu Sozeau | 24 March 2021, 11:53:03 UTC | WIP in positivity | 24 March 2021, 11:53:03 UTC |
| 608a915 | Matthieu Sozeau | 23 March 2021, 09:49:24 UTC | WIP in inductive inversion | 23 March 2021, 09:49:24 UTC |
| 8d9bc33 | Matthieu Sozeau | 23 March 2021, 01:59:29 UTC | WIP updating cumulativity proofs in inductive inversion | 23 March 2021, 01:59:29 UTC |
| e57be4d | Matthieu Sozeau | 22 March 2021, 22:40:28 UTC | Updated Validity ! | 22 March 2021, 22:40:28 UTC |
| 1f44455 | Matthieu Sozeau | 22 March 2021, 15:39:00 UTC | Finished updating PCUICSpine | 22 March 2021, 15:39:00 UTC |
| 0d15803 | Matthieu Sozeau | 18 March 2021, 22:02:35 UTC | WIP in PCUICSpine | 18 March 2021, 22:02:35 UTC |
| c849ae7 | Matthieu Sozeau | 18 March 2021, 02:50:34 UTC | WIP in Spines... | 18 March 2021, 02:50:34 UTC |
| f03ebaa | Matthieu Sozeau | 18 March 2021, 01:33:11 UTC | More cleanups and renamings | 18 March 2021, 01:33:11 UTC |
| f6404aa | Matthieu Sozeau | 18 March 2021, 00:16:48 UTC | WIP in Arities | 18 March 2021, 00:16:48 UTC |
| c6f9184 | Matthieu Sozeau | 17 March 2021, 12:39:47 UTC | Comment in conversion | 17 March 2021, 12:39:47 UTC |
| d27cf37 | Matthieu Sozeau | 17 March 2021, 12:34:35 UTC | Uniform naming scheme for conversion/cumulativity lemmas | 17 March 2021, 12:34:35 UTC |
| d72b8b2 | Matthieu Sozeau | 17 March 2021, 10:49:22 UTC | Updated PCUICContexts | 17 March 2021, 10:49:22 UTC |
| 4c3a453 | Matthieu Sozeau | 17 March 2021, 00:14:31 UTC | Moved inversion lemmas to well-scoped conversion | 17 March 2021, 00:14:31 UTC |
| 7dc4836 | Matthieu Sozeau | 16 March 2021, 19:51:15 UTC | Finished updating conversion lemmas! Now for the more interesting stuff :) | 16 March 2021, 23:04:14 UTC |
| b9bfecf | Matthieu Sozeau | 16 March 2021, 02:05:15 UTC | Higher-level lemmas of conversion | 16 March 2021, 02:05:15 UTC |
| 2d81b05 | Matthieu Sozeau | 16 March 2021, 01:39:18 UTC | Finally finished inversion lemmas on conv/cumulativity | 16 March 2021, 01:39:18 UTC |
| c7fb7ea | Matthieu Sozeau | 12 March 2021, 21:38:43 UTC | WIP in conversion | 12 March 2021, 21:38:43 UTC |
| 7072eec | Matthieu Sozeau | 12 March 2021, 14:38:02 UTC | Changing notations | 12 March 2021, 14:46:28 UTC |
| daacfdb | Matthieu Sozeau | 12 March 2021, 14:28:28 UTC | Updating Conversion | 12 March 2021, 14:28:28 UTC |
| acc8fad | Matthieu Sozeau | 12 March 2021, 12:21:47 UTC | Finished updating context conversion | 12 March 2021, 12:21:47 UTC |
| 06e7637 | Matthieu Sozeau | 11 March 2021, 20:54:13 UTC | WIP updating context conversion, with much cleaner proofs | 11 March 2021, 20:54:13 UTC |
| 3fb2d72 | Matthieu Sozeau | 10 March 2021, 22:58:19 UTC | Finished context conversion proof | 10 March 2021, 22:58:19 UTC |
| a3aa142 | Matthieu Sozeau | 09 March 2021, 15:30:44 UTC | Convext conversion proof | 09 March 2021, 15:30:44 UTC |
| 2bc7c32 | Matthieu Sozeau | 08 March 2021, 19:14:19 UTC | Completed confluence proofs | 08 March 2021, 19:14:19 UTC |
| e009d9f | Matthieu Sozeau | 08 March 2021, 10:44:44 UTC | Almost finished with confluence... | 08 March 2021, 10:44:44 UTC |
| eefe8e8 | Matthieu Sozeau | 08 March 2021, 00:19:59 UTC | WIP adapting confluence: now applies on well-scoped terms only | 08 March 2021, 00:19:59 UTC |
| 6abad1e | Matthieu Sozeau | 06 March 2021, 18:44:27 UTC | Refactorings | 06 March 2021, 18:44:27 UTC |
| b65c047 | Matthieu Sozeau | 06 March 2021, 17:49:16 UTC | pred1_ctx_pred1 needs well-scopedness assumptions | 06 March 2021, 17:49:16 UTC |
| aca5e2f | Matthieu Sozeau | 06 March 2021, 10:20:06 UTC | Updated Confluence | 06 March 2021, 10:20:06 UTC |
| 3fbc918 | Matthieu Sozeau | 05 March 2021, 19:05:02 UTC | todo-free confluence proof | 05 March 2021, 19:05:02 UTC |
| fc8a89b | Matthieu Sozeau | 04 March 2021, 12:36:07 UTC | WIP proving that pred1 preserves free variables | 04 March 2021, 12:36:07 UTC |
| 97d5e17 | Matthieu Sozeau | 04 March 2021, 11:57:19 UTC | Finished proof of confluence with "fixed" contexts | 04 March 2021, 11:57:19 UTC |
| cbc00cd | Matthieu Sozeau | 04 March 2021, 01:40:55 UTC | Generalized triangle lemma to allow any appropriate "join" context to be passed. | 04 March 2021, 01:40:55 UTC |
| 03f0316 | Matthieu Sozeau | 03 March 2021, 19:06:54 UTC | Issue in confluence with the "fixed" contexts | 03 March 2021, 19:06:54 UTC |
| 8bf738c | Matthieu Sozeau | 02 March 2021, 16:51:07 UTC | Finished definition of rho and proof of invariance by renaming | 02 March 2021, 16:51:07 UTC |
| af01812 | Matthieu Sozeau | 02 March 2021, 10:58:06 UTC | Finished parallel reduction theory | 02 March 2021, 10:58:06 UTC |
| 8aba9a5 | Matthieu Sozeau | 26 February 2021, 11:56:37 UTC | Closer to correct statement for on_free_vars side-conditions in parallel reduction | 01 March 2021, 20:53:39 UTC |
| 66b39da | Matthieu Sozeau | 26 February 2021, 02:27:12 UTC | Proven substituion and strong substitution simultaneously | 26 February 2021, 02:27:12 UTC |
