| 2e5d12f | Meven | 03 September 2020, 12:50:30 UTC | improved utils | 03 September 2020, 12:50:30 UTC |
| 3f96ea7 | Meven | 03 September 2020, 12:49:40 UTC | gradual stuff | 03 September 2020, 12:49:40 UTC |
| afd73e7 | SimonBoulier | 02 September 2020, 11:57:42 UTC | Reduce argument before calling tmFreshName | 02 September 2020, 13:08:24 UTC |
| 04d0e8c | Matthieu Sozeau | 02 September 2020, 07:49:28 UTC | Merge pull request #426 from MetaCoq/cumulative-inductives Cumulative inductive types | 02 September 2020, 07:49:28 UTC |
| c7780e8 | Matthieu Sozeau | 01 September 2020, 15:42:45 UTC | Move lemmas to their appropriate places | 01 September 2020, 15:42:45 UTC |
| 640e7d6 | Matthieu Sozeau | 31 August 2020, 16:18:47 UTC | Move new cumulativity relation to a separate library | 31 August 2020, 16:28:15 UTC |
| 2df91e5 | Matthieu Sozeau | 31 August 2020, 15:34:59 UTC | Finished typing_leq_term proof | 31 August 2020, 15:34:59 UTC |
| a0d88f6 | Matthieu Sozeau | 30 August 2020, 14:29:06 UTC | Introduce a new T ~ T' relation for convertibility up-to universes, relating prop to prop and Type i to any Type j. This allows proving that typable terms related by leq_term are equally erasable, even in presence of cumulative inductive types | 30 August 2020, 14:29:06 UTC |
| e1ad2df | Matthieu Sozeau | 27 August 2020, 16:58:44 UTC | WIP proving that leq_terms have the same typings in Prop (inductive cumulativity doesn't allow Prop/Type confusion) | 27 August 2020, 16:58:44 UTC |
| 501e3e2 | Matthieu Sozeau | 27 August 2020, 13:45:38 UTC | Adapt to new definition of eq_term/leq_term | 27 August 2020, 13:45:38 UTC |
| aabec06 | Matthieu Sozeau | 26 August 2020, 09:45:31 UTC | Adapt Principality to Cumulative Inductives | 26 August 2020, 09:45:31 UTC |
| e28f66c | Matthieu Sozeau | 06 July 2020, 16:05:38 UTC | SR proof finished for Case + cumulative inductives | 25 August 2020, 13:24:59 UTC |
| caf5ae8 | Matthieu Sozeau | 03 July 2020, 15:34:48 UTC | Progress on SR proof | 25 August 2020, 13:24:59 UTC |
| f3a6219 | Matthieu Sozeau | 02 July 2020, 17:39:25 UTC | WIP proving SR for cumulative inductives | 25 August 2020, 13:24:58 UTC |
| 9ef18fc | Matthieu Sozeau | 30 June 2020, 11:23:28 UTC | WIP | 25 August 2020, 13:24:58 UTC |
| 062f09b | Matthieu Sozeau | 16 June 2020, 14:22:25 UTC | WIP | 25 August 2020, 13:24:58 UTC |
| 3e88452 | Matthieu Sozeau | 29 May 2020, 10:32:19 UTC | Formalise validity of constructor types w.r.t. variance annotations | 25 August 2020, 13:24:58 UTC |
| 6c98072 | Matthieu Sozeau | 28 May 2020, 21:04:03 UTC | Prove that indices of constructors are closed w.r.t params and args (no recursive mention of the inductive) | 25 August 2020, 13:24:58 UTC |
| 10347bb | Matthieu Sozeau | 28 May 2020, 16:27:18 UTC | WIP on SR proofs of iota red | 25 August 2020, 13:24:58 UTC |
| f99843c | Matthieu Sozeau | 28 May 2020, 16:27:07 UTC | Define positivity of constructor types, needed for cumulativity | 25 August 2020, 13:24:58 UTC |
| 55854b3 | Matthieu Sozeau | 28 May 2020, 11:05:04 UTC | Simplified SR proof for iota reduction, still WIP | 25 August 2020, 13:24:57 UTC |
| 5b5b6ac | Matthieu Sozeau | 27 May 2020, 16:53:29 UTC | Prove a new arity_spine principle for cumulative inductives | 25 August 2020, 13:24:57 UTC |
| 15dd4f0 | Matthieu Sozeau | 27 May 2020, 09:34:04 UTC | Adding a positivity check | 25 August 2020, 13:24:57 UTC |
| a980fed | Matthieu Sozeau | 26 May 2020, 17:41:07 UTC | Adapted inductive inversion | 25 August 2020, 13:24:57 UTC |
| e4e0070 | Matthieu Sozeau | 26 May 2020, 16:53:49 UTC | Adapt confluence to generalize equality | 25 August 2020, 13:24:57 UTC |
| 09a2aa3 | Matthieu Sozeau | 26 May 2020, 13:57:59 UTC | Update to generalized eqterm definition | 25 August 2020, 13:24:57 UTC |
| ea6604e | Matthieu Sozeau | 26 May 2020, 12:23:14 UTC | Generalize equality test to consider application lengthsNeeded for the proper modelization of cumulativity on inductive types which applies only to fully applied inductivea and constructors | 25 August 2020, 13:24:57 UTC |
| 14aeb2e | Matthieu Sozeau | 25 May 2020, 18:45:07 UTC | Stuck in SR proof | 25 August 2020, 13:24:56 UTC |
| d165f7f | Matthieu Sozeau | 25 May 2020, 18:01:13 UTC | Adapted PCUICAlpha | 25 August 2020, 13:24:56 UTC |
| d19e6a0 | Matthieu Sozeau | 25 May 2020, 17:37:02 UTC | Upto inductive inversion principles | 25 August 2020, 13:24:56 UTC |
| e5db562 | Matthieu Sozeau | 25 May 2020, 16:53:33 UTC | Adapt confluence to new eq_term | 25 August 2020, 13:24:56 UTC |
| 9555f6e | Matthieu Sozeau | 25 May 2020, 15:39:14 UTC | Adapt weakening / nameless to new eq_term | 25 August 2020, 13:24:56 UTC |
| ab60944 | Matthieu Sozeau | 25 May 2020, 14:51:32 UTC | Updated PCUICEquality: now syntactic equality depends on a global env | 25 August 2020, 13:24:56 UTC |
| e3de77e | Matthieu Sozeau | 25 May 2020, 11:27:58 UTC | Well-formed variance info on inductives | 25 August 2020, 13:24:56 UTC |
| 7d7c4ce | Matthieu Sozeau | 25 August 2020, 08:17:50 UTC | Merge pull request #456 from MetaCoq/erases_closed Fill the erases_closed proof | 25 August 2020, 08:17:50 UTC |
| f126933 | Matthieu Sozeau | 24 August 2020, 16:02:09 UTC | Fill the erases_closed proof | 24 August 2020, 16:02:09 UTC |
| b18ee48 | Matthieu Sozeau | 30 July 2020, 18:31:44 UTC | Merge pull request #448 from jakobbotsch/fix_erase_mfix Fix computation with erase_mfix when assuming well-formedness | 30 July 2020, 18:31:44 UTC |
| 2f9b000 | Jakob Botsch Nielsen | 30 July 2020, 12:33:24 UTC | Fix computation with erase_mfix | 30 July 2020, 12:33:24 UTC |
| 0095f78 | Danil | 29 July 2020, 11:16:01 UTC | Fix test | 30 July 2020, 08:57:16 UTC |
| 9fb201c | Danil | 29 July 2020, 08:56:11 UTC | `tmQuoteRecTransp` is a general command taking a boolean "bypass opacity" flag. `tmQuoteRec` is defined as `tmQuoteRecTransp true`. Split `TmQuote` to two commands, because the bypass opacity flag makes sence only for recursive quoting. | 30 July 2020, 08:57:16 UTC |
| ae7a75b | Danil | 28 July 2020, 11:11:21 UTC | Fix agruments to quote_term_rec | 30 July 2020, 08:57:16 UTC |
| b703502 | Danil | 28 July 2020, 10:29:15 UTC | Add `tmQuoteRecTransp` that respects the opaqueness settings and quotes only transparent dependencies (opaque dependencies are quoted without bodies). The original `tmQuoteRec` still works as before - bypasses the opaqueness and quotes all the dependencies. | 30 July 2020, 08:57:16 UTC |
| 71e124c | Matthieu Sozeau | 24 July 2020, 19:41:42 UTC | Merge pull request #437 from jakobbotsch/fix-evals Fix evaluation relations to compute properly with stuck fixpoints | 24 July 2020, 19:41:42 UTC |
| 02f5d8a | Jakob Botsch Nielsen | 07 July 2020, 14:32:09 UTC | Some cleanup | 07 July 2020, 14:32:09 UTC |
| c84b218 | Jakob Botsch Nielsen | 07 July 2020, 14:09:34 UTC | Prove fix_value case (except for part requiring canonicity) | 07 July 2020, 14:09:34 UTC |
| 52e545f | Jakob Botsch Nielsen | 07 July 2020, 13:02:40 UTC | Remove some unused lemmas | 07 July 2020, 13:02:40 UTC |
| 621958e | Jakob Botsch Nielsen | 07 July 2020, 12:58:11 UTC | Prove fix case in erases_correct | 07 July 2020, 12:58:11 UTC |
| f4181d2 | Jakob Botsch Nielsen | 03 July 2020, 14:53:55 UTC | Add todos, keep old proof but commented for fix/fix_value | 03 July 2020, 14:53:55 UTC |
| 0d98d07 | Jakob Botsch Nielsen | 03 July 2020, 14:46:12 UTC | Revert "Add some todos in erases_correct" This reverts commit 5d3c27eb1bbffd562f64272b42f610c812f8a510. | 03 July 2020, 14:46:12 UTC |
| 5d3c27e | Jakob Botsch Nielsen | 03 July 2020, 13:10:47 UTC | Add some todos in erases_correct | 03 July 2020, 13:10:47 UTC |
| 91ae5ab | Jakob Botsch Nielsen | 03 July 2020, 13:02:43 UTC | Fix Template Coq wcbv evaluation relation | 03 July 2020, 13:02:43 UTC |
| 8896fa0 | Jakob Botsch Nielsen | 02 July 2020, 15:23:55 UTC | Work on fix case | 02 July 2020, 15:23:55 UTC |
| af74bdc | Jakob Botsch Nielsen | 02 July 2020, 13:01:09 UTC | Clean up | 02 July 2020, 13:01:50 UTC |
| 58d99f8 | Jakob Botsch Nielsen | 02 July 2020, 12:59:33 UTC | Small ssreflect related clean up | 02 July 2020, 12:59:33 UTC |
| f3ea4d3 | Jakob Botsch Nielsen | 01 July 2020, 20:51:24 UTC | Minor changes | 01 July 2020, 20:51:24 UTC |
| f7a2427 | Jakob Botsch Nielsen | 01 July 2020, 20:20:54 UTC | Fix fix/fix_value rules and prove eval_deterministic | 01 July 2020, 20:20:54 UTC |
| d181ec7 | Matthieu Sozeau | 01 July 2020, 14:23:01 UTC | Clear universe axioms (#433) * Fill todounivs proofs in PCUICInductives * Removed todounivs entirely | 01 July 2020, 14:23:01 UTC |
| f6fad62 | Jakob Botsch Nielsen | 01 July 2020, 10:58:45 UTC | Some work on new evaluation relation | 01 July 2020, 10:58:45 UTC |
| dd9786c | Jakob Botsch Nielsen | 30 June 2020, 10:56:14 UTC | Erasure eval_fix_value ensure not box | 30 June 2020, 10:56:14 UTC |
| c259a6a | Matthieu Sozeau | 23 June 2020, 10:41:51 UTC | Update CI and chat links | 23 June 2020, 10:41:51 UTC |
| 9e0cfdc | SimonBoulier | 19 May 2020, 16:09:44 UTC | Add example | 26 May 2020, 08:46:02 UTC |
| 1cd94d1 | SimonBoulier | 19 May 2020, 16:04:52 UTC | Fix tmVariable | 26 May 2020, 08:46:02 UTC |
| 3336c60 | Yannick Forster | 19 May 2020, 14:40:01 UTC | Implement tmVariable command | 26 May 2020, 08:46:02 UTC |
| 53bb89d | SimonBoulier | 26 May 2020, 08:20:13 UTC | Delete old file | 26 May 2020, 08:45:38 UTC |
| a11db52 | SimonBoulier | 26 May 2020, 07:51:44 UTC | Fix Extractable monad test | 26 May 2020, 08:45:38 UTC |
| d0a140a | SimonBoulier | 22 May 2020, 10:32:36 UTC | Remove camlp4 stuffs | 26 May 2020, 08:45:38 UTC |
| 5e79580 | SimonBoulier | 22 May 2020, 10:26:17 UTC | Renaming modules, moving lot of code and removing unused code | 26 May 2020, 08:45:38 UTC |
| 5eae634 | SimonBoulier | 22 May 2020, 09:05:06 UTC | Rename Quoter + move reduce | 26 May 2020, 08:45:38 UTC |
| 1411936 | Matthieu Sozeau | 24 May 2020, 23:42:38 UTC | Confluence proven without the isLambda constraint | 26 May 2020, 07:02:39 UTC |
| 5c0c521 | Matthieu Sozeau | 20 May 2020, 19:34:29 UTC | Weaken pred1 a bit to not reduce "new" redexes | 26 May 2020, 07:02:39 UTC |
| ffdcb5b | Matthieu Sozeau | 20 May 2020, 19:09:45 UTC | Use views consistently in the definition of rho (simpler proofs!) | 26 May 2020, 07:02:39 UTC |
| 5042825 | Matthieu Sozeau | 20 May 2020, 16:11:52 UTC | Also prove unfolding lemma for fixpoint | 26 May 2020, 07:02:39 UTC |
| 1445eda | Matthieu Sozeau | 20 May 2020, 13:58:29 UTC | Add a new version of rho using Equations and a well-founded order | 26 May 2020, 07:02:39 UTC |
| 7aacc27 | Matthieu Sozeau | 20 May 2020, 19:35:57 UTC | Merge pull request #422 from MetaCoq/wffixpoints Well-formed (co)fixpoints | 20 May 2020, 19:35:57 UTC |
| 4da44e4 | Matthieu Sozeau | 19 May 2020, 22:55:19 UTC | Fix after rebase | 19 May 2020, 22:55:19 UTC |
| 618f97e | Matthieu Sozeau | 19 May 2020, 22:21:54 UTC | Adapt erasure to fix/cofix changes | 19 May 2020, 22:46:23 UTC |
| 6a0c679 | Matthieu Sozeau | 19 May 2020, 21:52:16 UTC | Remove now unused allow_cofix flag | 19 May 2020, 22:46:23 UTC |
| d75468d | Matthieu Sozeau | 19 May 2020, 21:32:52 UTC | Adapt SR proof to new well-formedness of fix and cofix | 19 May 2020, 22:46:23 UTC |
| 779937b | Matthieu Sozeau | 18 May 2020, 22:27:46 UTC | TODOs in TemplatetoPCUIC | 19 May 2020, 22:46:23 UTC |
| cf37a1a | Matthieu Sozeau | 04 July 2019, 06:14:31 UTC | cofix_guard and well-formed fixpoint/cofixpoint condition | 19 May 2020, 22:46:23 UTC |
| e03c681 | SimonBoulier | 12 May 2020, 15:33:18 UTC | Better reiication of kernames | 19 May 2020, 15:28:57 UTC |
| 6d1ab4c | Matthieu Sozeau | 19 May 2020, 07:49:12 UTC | Merge pull request #416 from MetaCoq/primproj Primitive projections | 19 May 2020, 07:49:12 UTC |
| 8d492ff | Matthieu Sozeau | 18 May 2020, 10:40:08 UTC | Remove unused Import and Derive causing opam failure | 18 May 2020, 10:40:08 UTC |
| b788a0b | Matthieu Sozeau | 15 May 2020, 11:36:21 UTC | Principality and all todos on projs finished | 15 May 2020, 19:13:06 UTC |
| bc897d1 | Matthieu Sozeau | 15 May 2020, 11:05:00 UTC | Finish principality proof for projections | 15 May 2020, 11:05:00 UTC |
| 6a1ea1b | Matthieu Sozeau | 15 May 2020, 09:51:21 UTC | Move lemmas from SR to the appropriate libraries | 15 May 2020, 10:07:09 UTC |
| 49c57ad | Matthieu Sozeau | 14 May 2020, 17:54:21 UTC | More refactorings, validity is clear | 15 May 2020, 08:58:31 UTC |
| 43b7804 | SimonBoulier | 15 May 2020, 07:52:24 UTC | Fix website link | 15 May 2020, 07:52:24 UTC |
| 284bb8b | Matthieu Sozeau | 14 May 2020, 16:48:16 UTC | More refactorings | 14 May 2020, 16:48:16 UTC |
| ce33e0b | Matthieu Sozeau | 13 May 2020, 17:06:26 UTC | Refactorings, add MCPrelude file | 14 May 2020, 14:37:28 UTC |
| 787191d | Vadim Zaliva | 13 May 2020, 00:32:28 UTC | compatbility with ocaml 4.10.0 | 14 May 2020, 13:46:33 UTC |
| 9cd5e54 | Matthieu Sozeau | 13 May 2020, 17:05:35 UTC | Refactor proofs | 13 May 2020, 17:05:35 UTC |
| fc9fd5c | Matthieu Sozeau | 13 May 2020, 11:14:32 UTC | Finish SR proofs for projections: congruence/cofix/iota reduction all proved | 13 May 2020, 11:15:59 UTC |
| 7d62dd5 | SimonBoulier | 12 May 2020, 15:25:13 UTC | Add a Test Unquote command | 12 May 2020, 16:59:23 UTC |
| c975d7f | Matthieu Sozeau | 12 May 2020, 16:17:57 UTC | Finish congruence case of projection: only cofix missing | 12 May 2020, 16:17:57 UTC |
| cc057f7 | Matthieu Sozeau | 12 May 2020, 15:58:33 UTC | Finished the projection reduction case of SR | 12 May 2020, 15:58:33 UTC |
| ab78354 | Matthieu Sozeau | 07 May 2020, 13:03:33 UTC | Proof of projection type validity | 07 May 2020, 20:01:18 UTC |
| f9863bc | Matthieu Sozeau | 01 May 2020, 10:58:57 UTC | Adapt PCUIC to new projection invariant | 07 May 2020, 18:43:29 UTC |
| b0c7190 | Matthieu Sozeau | 01 May 2020, 09:05:16 UTC | Adapt checker | 07 May 2020, 18:41:49 UTC |
| 51b3af6 | Matthieu Sozeau | 28 April 2020, 18:29:04 UTC | Reorganize constructor shape / invariants on inductives for more clarity | 07 May 2020, 18:41:49 UTC |
