| a6f9175 | SimonBoulier | 17 June 2020, 21:26:53 UTC | WIP | 17 June 2020, 21:26:53 UTC |
| 1077b79 | SimonBoulier | 17 June 2020, 10:21:17 UTC | WIP | 17 June 2020, 10:21:17 UTC |
| d59c1a9 | SimonBoulier | 16 June 2020, 15:14:57 UTC | WIP | 16 June 2020, 15:14:57 UTC |
| c2aef68 | SimonBoulier | 09 June 2020, 21:33:44 UTC | WIP | 09 June 2020, 21:33:44 UTC |
| 3a76905 | SimonBoulier | 08 June 2020, 15:26:58 UTC | WIP | 08 June 2020, 15:26:58 UTC |
| 33acbae | SimonBoulier | 03 June 2020, 14:07:36 UTC | WIP | 03 June 2020, 14:07:36 UTC |
| 594cc84 | SimonBoulier | 03 June 2020, 11:05:59 UTC | WIP | 03 June 2020, 11:05:59 UTC |
| df751e3 | SimonBoulier | 31 May 2020, 21:06:59 UTC | WIP | 31 May 2020, 21:06:59 UTC |
| 0d2bb84 | SimonBoulier | 27 May 2020, 16:39:58 UTC | WIP | 27 May 2020, 16:39:58 UTC |
| c84e0d0 | SimonBoulier | 27 May 2020, 15:43:41 UTC | WIP | 27 May 2020, 15:43:41 UTC |
| 5444cf4 | SimonBoulier | 27 May 2020, 10:07:55 UTC | eta confluence ! | 27 May 2020, 10:07:55 UTC |
| fdc26a7 | SimonBoulier | 27 May 2020, 09:05:21 UTC | eta confl upto fix | 27 May 2020, 09:05:21 UTC |
| c8adb76 | SimonBoulier | 26 May 2020, 09:05:54 UTC | fix | 26 May 2020, 09:05:54 UTC |
| 82dc2a4 | SimonBoulier | 26 May 2020, 08:32:12 UTC | WIP | 26 May 2020, 08:41:29 UTC |
| 767045d | SimonBoulier | 23 April 2020, 15:07:48 UTC | WIP | 26 May 2020, 08:41:29 UTC |
| 40fdd4d | SimonBoulier | 23 April 2020, 10:31:01 UTC | red1_eta_ctx | 26 May 2020, 08:41:29 UTC |
| 8fc3253 | SimonBoulier | 22 April 2020, 16:02:44 UTC | WIP | 26 May 2020, 08:41:29 UTC |
| ad738d2 | SimonBoulier | 21 April 2020, 09:40:47 UTC | WIP | 26 May 2020, 08:41:29 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 |
| 8054e0c | Matthieu Sozeau | 21 April 2020, 16:38:32 UTC | Typing of primitive projection declarations | 07 May 2020, 18:41:49 UTC |
| 22c7bf2 | Matthieu Sozeau | 29 April 2020, 09:59:35 UTC | Merge pull request #414 from MetaCoq/univ_lemma Universe lemmas | 29 April 2020, 09:59:35 UTC |
| 9f0ff8d | SimonBoulier | 29 April 2020, 09:12:45 UTC | Universe lemmas | 29 April 2020, 09:12:45 UTC |
| 9974965 | Matthieu Sozeau | 28 April 2020, 12:23:34 UTC | Merge pull request #413 from MetaCoq/move-typing-leq-term Move typing_leq_term to Principality | 28 April 2020, 12:23:34 UTC |
| 5c48885 | Matthieu Sozeau | 28 April 2020, 11:25:25 UTC | Update README.md | 28 April 2020, 11:25:25 UTC |
| 0e95f94 | Matthieu Sozeau | 28 April 2020, 11:13:38 UTC | Move typing_leq_term to Principality | 28 April 2020, 11:14:28 UTC |
| de9bb81 | Matthieu Sozeau | 28 April 2020, 11:14:02 UTC | Merge pull request #412 from MetaCoq/move-universes Move universe-related admits to Universes | 28 April 2020, 11:14:02 UTC |
| 5624edc | Matthieu Sozeau | 28 April 2020, 10:43:35 UTC | More refactorings | 28 April 2020, 10:43:35 UTC |
| 85572a7 | Matthieu Sozeau | 27 April 2020, 15:32:08 UTC | Move universe-related admits to Universes | 27 April 2020, 15:58:36 UTC |
| fbd85f1 | Matthieu Sozeau | 27 April 2020, 09:26:54 UTC | Merge pull request #411 from MetaCoq/eliminations Fill proofs about elimination restrictions | 27 April 2020, 09:26:54 UTC |
| 78cedbc | Matthieu Sozeau | 25 April 2020, 10:42:15 UTC | Finish a proof in PCUICArities | 25 April 2020, 10:42:15 UTC |
| ff7b8ce | Matthieu Sozeau | 25 April 2020, 09:43:46 UTC | Finish typing_leq_term proof | 25 April 2020, 09:46:02 UTC |
| f894c17 | Matthieu Sozeau | 24 April 2020, 20:24:01 UTC | Add necessary isWAT preconditions to cumul_props It is slightly subtle to prove that if B : Prop and A <= B then A cannot actually be>1;95;0c an arity, so we indeed get the conclusions of the theorems in full generality! | 24 April 2020, 20:56:31 UTC |
| ffd0847 | Matthieu Sozeau | 24 April 2020, 10:19:58 UTC | Uncomment case erasure proof | 24 April 2020, 10:19:58 UTC |
| 3fb9372 | Matthieu Sozeau | 23 April 2020, 18:55:41 UTC | Finished the elimination principle proofs for case and proj | 24 April 2020, 09:19:18 UTC |
| d6699bf | Matthieu Sozeau | 22 April 2020, 09:40:35 UTC | Merge pull request #408 from MetaCoq/NeuralCoder3/coq-8.11 NeuralCoder3/coq 8.11 fixed for merging | 22 April 2020, 09:40:35 UTC |
| 8741dca | Yannick Forster | 22 April 2020, 07:03:38 UTC | Remove typo | 22 April 2020, 07:03:38 UTC |
| 636e2b3 | Matthieu Sozeau | 21 April 2020, 17:01:21 UTC | Merge pull request #406 from MetaCoq/safeadmits Turn one admit into a todo on projections, an prove wellformed_R_pres | 21 April 2020, 17:01:21 UTC |
| f27adef | Matthieu Sozeau | 21 April 2020, 16:59:50 UTC | Merge pull request #407 from fakusb/inferInstanceFixUniverses Remove universe constraint between "option" and (non-extractable) Template Monad | 21 April 2020, 16:59:50 UTC |
| f20240d | Matthieu Sozeau | 21 April 2020, 16:54:25 UTC | Fix before merge, changes in Fix/CoFix typing rules and typing_ind_env | 21 April 2020, 16:54:25 UTC |
| 207d7d5 | Marcel Ullrich | 03 April 2020, 16:28:50 UTC | avoided Checker | 21 April 2020, 16:43:26 UTC |
| 93b0a06 | Marcel Ullrich | 03 April 2020, 15:03:57 UTC | organized imports | 21 April 2020, 16:43:26 UTC |
| b511be6 | Marcel Ullrich | 03 April 2020, 11:59:30 UTC | removed print statements | 21 April 2020, 16:43:25 UTC |
| c17c48d | Marcel Ullrich | 03 April 2020, 11:58:13 UTC | added conversion to project file | 21 April 2020, 16:43:25 UTC |
| a93682d | Marcel Ullrich | 03 April 2020, 11:56:17 UTC | cleanup | 21 April 2020, 16:43:25 UTC |
| cd45696 | Marcel Ullrich | 03 April 2020, 11:43:17 UTC | added pcuic -> template conversion | 21 April 2020, 16:43:25 UTC |
| edaaa79 | Marcel Ullrich | 03 April 2020, 11:42:50 UTC | cleanup | 21 April 2020, 16:43:25 UTC |
| 57399a6 | Marcel Ullrich | 03 April 2020, 11:36:11 UTC | added correctness for pcuic -> template | 21 April 2020, 16:43:25 UTC |
| 3ef054d | Marcel Ullrich | 03 April 2020, 11:35:28 UTC | added conversion | 21 April 2020, 16:43:24 UTC |
| 4c478c9 | Fabian Kunze | 21 April 2020, 15:23:35 UTC | added test file that checks that no universe constrain on option is generated. | 21 April 2020, 15:23:35 UTC |
| 4221abb | Matthieu Sozeau | 21 April 2020, 14:26:38 UTC | Turn one admit into a todo on projections, an prove wellformed_R_pres | 21 April 2020, 14:26:38 UTC |
| 69ca42b | Matthieu Sozeau | 21 April 2020, 13:37:32 UTC | Merge pull request #405 from MetaCoq/nostrengthening No strengthening | 21 April 2020, 13:37:32 UTC |
| a967034 | Matthieu Sozeau | 21 April 2020, 12:26:28 UTC | Remove strengthening axiom (now unnecessary) | 21 April 2020, 12:57:43 UTC |
| 7ac9319 | Matthieu Sozeau | 21 April 2020, 12:21:37 UTC | Fix safechecker | 21 April 2020, 12:57:43 UTC |
| a2eef73 | Matthieu Sozeau | 21 April 2020, 11:33:02 UTC | More sigma calculus cleanup | 21 April 2020, 12:57:43 UTC |
| e78350a | Fabian Kunze | 12 July 2019, 10:02:43 UTC | moved result of tryInferInstance to copy of option type to fix universe problem | 21 April 2020, 12:39:50 UTC |
| ecb955b | Matthieu Sozeau | 20 April 2020, 13:37:21 UTC | Merge pull request #404 from MetaCoq/cleanup-sigmacalc Fill some admitted proofs and move sigma-calculus lemmas together | 20 April 2020, 13:37:21 UTC |
| 4cccc61 | Matthieu Sozeau | 20 April 2020, 11:31:12 UTC | Fill some admitted proofs and move sigma-calculus lemmas together | 20 April 2020, 13:05:48 UTC |
| 20a1c1d | SimonBoulier | 20 April 2020, 10:57:46 UTC | Add guidelines in Readme | 20 April 2020, 10:59:14 UTC |
| ae3f353 | SimonBoulier | 20 April 2020, 08:56:33 UTC | Merge branch 'conversion-proofs' into coq-8.11 | 20 April 2020, 10:56:06 UTC |
| 1b8289b | SimonBoulier | 17 April 2020, 14:36:53 UTC | Remove Program form template-coq and pcuic | 20 April 2020, 08:49:38 UTC |
| 64947d3 | Matthieu Sozeau | 18 April 2020, 16:06:27 UTC | Fill admittted proofs in Confluence/Conversion etc.. | 18 April 2020, 16:35:53 UTC |
| eeb166a | Matthieu Sozeau | 17 April 2020, 11:18:28 UTC | Merge pull request #399 from MetaCoq/validity-principality Validity principality | 17 April 2020, 11:18:28 UTC |
| f32ef34 | Matthieu Sozeau | 16 April 2020, 15:34:08 UTC | Adapt erasure to a name change | 16 April 2020, 15:39:05 UTC |
| 10083e8 | Matthieu Sozeau | 16 April 2020, 15:21:43 UTC | Finish principality except for case and proj | 16 April 2020, 15:39:04 UTC |
| f7cbc49 | Matthieu Sozeau | 16 April 2020, 13:43:57 UTC | Finished validity proof | 16 April 2020, 15:39:04 UTC |
| 15e8480 | Matthieu Sozeau | 15 April 2020, 21:03:46 UTC | Fix pose proof (id := ) not in 8.11 | 16 April 2020, 10:47:47 UTC |
| d324955 | Matthieu Sozeau | 15 April 2020, 19:41:22 UTC | Adapt | 16 April 2020, 10:47:47 UTC |
| 0feffce | Matthieu Sozeau | 15 April 2020, 15:38:29 UTC | Adapt safe retyping to new validity statement | 16 April 2020, 10:47:47 UTC |
| 2ca0bf9 | Matthieu Sozeau | 15 April 2020, 15:34:38 UTC | Adapt Safe Checker to new fix typing rule (simpler!) | 16 April 2020, 10:47:47 UTC |
