| HEAD | 8d576c7 | Merge pull request #538 from jakobbotsch/eval-no-axioms Remove evaluation of axioms from wcbv and add proof of consistency using safe reduction + canonicity | 04 January 2021, 09:30:58 UTC |
| refs/heads/TemplateMonadToTM | d76226c | some work on automatic translation from TemplateMonad to TM | 25 October 2019, 16:07:27 UTC |
| refs/heads/anonymized | d609826 | Update README.md | 11 July 2019, 11:27:39 UTC |
| refs/heads/bidirectional | f159ba2 | Merge remote-tracking branch 'origin/bidirectional' into bidirectional | 20 January 2021, 11:19:55 UTC |
| refs/heads/case-representation-bidir | fef963e | BDStrengthening, missing computation + the annoying cases | 04 June 2021, 15:31:56 UTC |
| refs/heads/check-fix | 19d43e2 | WIP updating the proofs | 05 July 2019, 16:30:28 UTC |
| refs/heads/clean | 1887074 | Commit HTML doc | 20 September 2019, 11:28:28 UTC |
| refs/heads/clean-ugraph | c3703b0 | clean ugraph | 11 July 2019, 09:45:38 UTC |
| refs/heads/complete-conversion | b4c8c44 | Completing the Conversion file | 25 July 2019, 06:14:10 UTC |
| refs/heads/conv_lemmas | 03d3eb0 | A few conv lemmas in SafeLemmata | 11 September 2019, 16:34:42 UTC |
| refs/heads/coq-8.10 | b960d7d | Fixed univ.v issue | 03 March 2020, 15:30:31 UTC |
| refs/heads/coq-8.11 | 8d576c7 | Merge pull request #538 from jakobbotsch/eval-no-axioms Remove evaluation of axioms from wcbv and add proof of consistency using safe reduction + canonicity | 04 January 2021, 09:30:58 UTC |
| refs/heads/coq-8.12 | ebcd89f | Merge pull request #540 from yforster/coq-8.12-jan18 Preparing for `coq-metacoq.1.0~beta2+8.12` | 19 January 2021, 14:59:22 UTC |
| refs/heads/coq-8.5 | ddcf94e | Drastic performance improvement Share string by hashconsing the string objects (reduces memory consumption by half on the Gcd example of certicoq). We do it for whole idents right now, the current Coq string representation does not allow to share prefixes sadly. Also remove the externalisation + elaboration phases when introducing quoted terms, we can bypass it completely and give the term directly for the kernel to check (without bypassing any checks though!). There is still an inefficiency due to retypechecking strings which does not seem so easy to avoid. We went from 240s to 24s when quoting CertiCoq's Gcd example. | 13 December 2016, 14:17:09 UTC |
| refs/heads/coq-8.6 | b1106ec | Update gitignore | 20 October 2017, 10:33:47 UTC |
| refs/heads/coq-8.7 | 1b47bab | Fix Extraction? | 29 May 2018, 09:44:08 UTC |
| refs/heads/coq-8.8 | 500e67e | Merge pull request #314 from MetaCoq/conv-args-coq8.8-again More symmetric approach to conversion of stacks (again 8.8) | 15 October 2019, 15:26:05 UTC |
| refs/heads/coq-8.9 | f06610a | do not capture the exceptions of the continuation | 31 January 2020, 14:10:31 UTC |
| refs/heads/correct_check_correct_arity | 659de9d | [WIP] Compile jusque extraction sauf plugin | 07 November 2019, 15:13:07 UTC |
| refs/heads/dependencies | 9979d60 | support for Extractable.tmDependencies. | 30 April 2019, 21:41:48 UTC |
| refs/heads/double_trans | a1532eb | WIP | 20 May 2020, 12:21:59 UTC |
| refs/heads/erasure-retyping-switch-letpattern-bug | 1647e10 | WIP on safe retyping | 10 September 2019, 10:11:04 UTC |
| refs/heads/eta | 24f6110 | [WIP] Fail to add η-conversion to eq_term | 25 November 2019, 14:08:56 UTC |
| refs/heads/eta-equality | e0f3026 | congruence closure with conv_pb to handle co-/equivariance | 31 May 2021, 11:05:35 UTC |
| refs/heads/eta_postpo | df751e3 | WIP | 31 May 2020, 21:06:59 UTC |
| refs/heads/ewcbveval-evalfix | 0abd687 | Fix EWcbvEval fix evaluation rule, spotted by R. Pollack | 15 August 2019, 18:35:31 UTC |
| refs/heads/extractable-translation_utils | bacd547 | adding `Generate Definition` and use for generating definitions. | 07 June 2019, 18:24:24 UTC |
| refs/heads/extraction_extraction | 95a10bb | A try at extraction: scheme seems to work but we need a printer for ascii | 23 July 2019, 20:43:51 UTC |
| refs/heads/generalizing_pred | a6f9175 | WIP | 17 June 2020, 21:26:53 UTC |
| refs/heads/gradual-CIC | 2e5d12f | improved utils | 03 September 2020, 12:50:30 UTC |
| refs/heads/infer_complete | 932891b | Remove one use of strengthening in infer | 29 January 2020, 13:25:28 UTC |
| refs/heads/itp-artefact | 2d631dc | adapting the README | 03 February 2021, 23:41:40 UTC |
| refs/heads/master | 69bb96e | Merge pull request #457 from maximedenes/fix-refine-order Avoid relying on subgoals order for refine | 01 September 2020, 12:36:31 UTC |
| refs/heads/master-merge-8.11 | 90bf648 | Fix for lia being stronger (on boolean goals) | 22 June 2020, 18:18:27 UTC |
| refs/heads/module-path-inequality | 793a036 | Add -bin-annot option | 19 July 2019, 00:24:09 UTC |
| refs/heads/new_repr_univs | 17fe0df | WIP | 27 February 2020, 16:26:22 UTC |
| refs/heads/old-unsafe-checker | 12e27f6 | Add HoTT test for checker | 19 September 2019, 10:18:10 UTC |
| refs/heads/pcuic-induction | 1bddd51 | WIP on PCUICReduction: congruence lemmas for `red` | 25 March 2019, 14:50:11 UTC |
| refs/heads/pcuic-infer | 6e8787b | fix compilation | 05 July 2019, 14:36:35 UTC |
| refs/heads/pcuic-plugin-fixups | a79cb91 | Update .gitignore | 09 September 2019, 13:21:11 UTC |
| refs/heads/popl-artifact-eval | eff8fe1 | In the ci-opam case, also remove the packages This avoids confusing the opam cache, which might think it does not have to recompile some packages | 16 November 2019, 14:28:38 UTC |
| refs/heads/quickchick | 5c16f2b | A try at mutation testing | 12 July 2019, 19:35:07 UTC |
| refs/heads/remove_pcuic_plugin | 2b6368c | Remove useless plugin | 23 August 2019, 13:27:32 UTC |
| refs/heads/safechecker | f74dd99 | Merge pull request #218 from yforster/safechecker-univs Safe checker with universes | 11 July 2019, 04:53:52 UTC |
| refs/heads/ssr-compat | 6c45bfc | WIP fixing compilation of plugins | 07 June 2019, 15:01:16 UTC |
| refs/heads/tauto | 5856a0b | renaming | 18 October 2019, 09:19:35 UTC |
| refs/heads/to_mie | e1d8530 | finished, but untested to_mie - unifying `Univ.constraint_type`, `Univ.Variance.t`, `Sorts.family` | 05 May 2019, 21:46:30 UTC |
| refs/heads/univalent-parametricity-errors | 1cf0438 | Paste error message in FP | 13 November 2019, 11:11:35 UTC |
| refs/heads/univalent-parametricity-errors2 | 2f62853 | WIP | 24 February 2020, 08:39:06 UTC |
| refs/heads/univalent_parametricity | 422e54d | [WIP] bug in conversion in test with conv_context in check_correct_arity | 06 November 2019, 16:30:48 UTC |
| refs/heads/wellformed_nlctx | 1417cef | Prove wellformed_nlctx | 16 September 2019, 11:37:11 UTC |
| refs/heads/yannick_axioms | 6e1172b | Work on prop_sub_type for Yannick | 21 October 2019, 15:57:24 UTC |
| refs/tags/1.0-alpha+8.8 | 5e95cc0 | Add extraction with time bounds reference in the Papers section | 27 September 2019, 16:26:10 UTC |
| refs/tags/1.0-alpha+8.9 | 8cecb1b | Add extraction with time bounds reference in the Papers section | 27 September 2019, 16:26:10 UTC |
| refs/tags/CoqCoqCorrect | 914e4c6 | Also mention Théo's README.md files in pcuic/ and safechecker/ | 16 November 2019, 13:22:14 UTC |
| refs/tags/v1.0-alpha2-8.10 | b960d7d | Fixed univ.v issue | 03 March 2020, 15:30:31 UTC |
| refs/tags/v1.0-alpha2-8.11 | ba0c595 | Big change in universes: - change the representation of UnivExpr - change the representation of universes (sorted, non empty list w/o duplicate) - prove completness of the comparison algorithm | 07 February 2020, 22:27:35 UTC |
| refs/tags/v2.0-beta | 33529a2 | Backport README and LICENSE changes from master branch | 15 February 2018, 15:10:27 UTC |
| refs/tags/v2.1-beta | c381f51 | Use better reduction functions | 04 July 2018, 14:06:40 UTC |
| refs/tags/v2.1-beta2 | c81ffca | Merge pull request #25 from Template-Coq/wcbveval Weak call-by-value evaluation definition | 08 August 2018, 10:19:20 UTC |
| refs/tags/v2.1-beta3 | a02e9bf | Update gitignore | 13 August 2018, 23:35:58 UTC |
