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 |
8eb47ec | Matthieu Sozeau | 15 April 2020, 15:06:51 UTC | Clean SafeLemmata of now now proven lemmas | 16 April 2020, 10:47:47 UTC |
0572011 | Matthieu Sozeau | 15 April 2020, 14:34:14 UTC | Remove commented valid_btys lemma and add todo for Simon | 16 April 2020, 10:47:47 UTC |
553995a | Matthieu Sozeau | 15 April 2020, 14:20:41 UTC | Admit-free Subject Reduction proof (projections are TODOs) | 16 April 2020, 10:47:47 UTC |
3408d59 | Matthieu Sozeau | 15 April 2020, 11:56:06 UTC | Closed all gaps in case SR proof | 16 April 2020, 10:47:47 UTC |
6f0845d | Matthieu Sozeau | 14 April 2020, 20:08:12 UTC | Completed all_rels_subst proof | 16 April 2020, 10:47:47 UTC |
4229021 | Matthieu Sozeau | 14 April 2020, 16:56:58 UTC | More moving of lemmas. One important admit left in PCUICSpine | 16 April 2020, 10:47:47 UTC |
7d79dae | Matthieu Sozeau | 14 April 2020, 16:10:31 UTC | Lots of refactorings and cleanups | 16 April 2020, 10:47:47 UTC |