| 90bf648 | Matthieu Sozeau | 22 June 2020, 18:18:27 UTC | Fix for lia being stronger (on boolean goals) | 22 June 2020, 18:18:27 UTC |
| 3247b25 | Matthieu Sozeau | 22 June 2020, 17:59:00 UTC | Fix a warning | 22 June 2020, 17:59:00 UTC |
| dbd7c81 | Matthieu Sozeau | 22 June 2020, 16:58:01 UTC | Fix after merge of 8.11 | 22 June 2020, 17:52:16 UTC |
| ff3be88 | Matthieu Sozeau | 22 June 2020, 12:36:29 UTC | Merge branch 'coq-8.11' | 22 June 2020, 12:36:29 UTC |
| 5169bae | Matthieu Sozeau | 22 June 2020, 12:27:27 UTC | Fix script | 22 June 2020, 12:27:27 UTC |
| b1e4eb5 | Matthieu Sozeau | 16 June 2020, 13:18:25 UTC | Merge pull request #428 from MetaCoq/noconf-fix depelim and noconfusion fixes | 16 June 2020, 13:18:25 UTC |
| 0822da8 | Matthieu Sozeau | 16 June 2020, 11:24:39 UTC | Fixed noconfusion doing too much hnf | 16 June 2020, 11:30:59 UTC |
| 432e928 | Matthieu Sozeau | 16 June 2020, 10:46:47 UTC | Adapt to fix in Equations for simplification up-to reduction | 16 June 2020, 10:47:00 UTC |
| 5425f20 | Matthieu Sozeau | 15 June 2020, 15:55:12 UTC | Merge pull request #427 from MetaCoq/equations-master-fix Fix for latest master version of Equations (depelim fixed) | 15 June 2020, 15:55:12 UTC |
| 34a4674 | Matthieu Sozeau | 15 June 2020, 14:18:12 UTC | Fix for latest master version of Equations (depelim fixed) | 15 June 2020, 15:18:19 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 |
| 4e6d6df | Pierre Roux | 28 March 2020, 21:10:49 UTC | [coq] Adapt to coq/coq#11948 | 15 May 2020, 16:28:38 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 |
| 526e6b1 | Matthieu Sozeau | 07 May 2020, 20:04:06 UTC | Merge pull request #415 from herbelin/master+pr12146-subst-restricted-on-secvar Adapt to Coq PR #12146: tactic subst now inactive on section variables with indirect dependency in goal | 07 May 2020, 20:04:06 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 |
| 17a8473 | Hugo Herbelin | 02 May 2020, 21:08:36 UTC | Adapt to subst not substituting section variables with indirect dependencies. | 02 May 2020, 21:08:36 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 |
| 1f9c9fe | Matthieu Sozeau | 27 April 2020, 12:25:55 UTC | Merge branch 'coq-8.11' | 27 April 2020, 12:25:55 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 |
| 51b4396 | Matthieu Sozeau | 24 April 2020, 13:32:10 UTC | Merge pull request #402 from herbelin/master+pr12023-atomic-tactic-now-qualified-in-ltac-file Moving names of primitive atomic tactics from Coq.Init.Notations to Coq.Init.Ltac | 24 April 2020, 13:32:10 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 |
| 6080c84 | Hugo Herbelin | 18 April 2020, 14:13:31 UTC | Adapting to Coq PR #12023: atomic form of primitive tactics are in module Ltac. Previously, it was in Coq.Init.Notations. Now in Coq.Init.Ltac. | 22 April 2020, 11:56:55 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 |
| 5c9720e | Pierre-Marie Pédrot | 06 April 2020, 13:44:40 UTC | Fix w.r.t. coq/coq#11896. | 21 April 2020, 12:16:55 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 |
