aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-08-26Better encapsulation of future goalsMaxime Dénès
2020-08-26Merge PR #12764: A fix and two enhancements of trailing pattern factorization...Pierre-Marie Pédrot
2020-08-26Merge PR #12904: Move bench job definition to its own filePierre-Marie Pédrot
2020-08-26Merge PR #12881: Deprecate intro_usingPierre-Marie Pédrot
2020-08-26Merge PR #12901: [bench] Remove useless commit guessing logicPierre-Marie Pédrot
2020-08-26Merge PR #12884: Documentation of coq_makefile: fix name of installation dir ...coqbot-app[bot]
2020-08-26Merge PR #12861: Require NsatzTactic: nsatz support for Z and QPierre-Marie Pédrot
2020-08-25Documentation of coq_makefile: fix name of installation dir + help on option -f.Hugo Herbelin
2020-08-25Moving production_level_eq to extend.ml for separation of concerns.Hugo Herbelin
2020-08-25A fix and two enhancements of trailing pattern factorization in rec. notations.Hugo Herbelin
2020-08-25Move bench job definition to its own fileGaëtan Gilbert
2020-08-25Require NsatzTactic: nsatz support for Z and QJason Gross
2020-08-25Remove useless commit guessing logicJason Gross
2020-08-25Merge PR #12879: added numeral_notation to META.coq.incoqbot-app[bot]
2020-08-25Merge PR #12897: [test-suite] close the proof added in #12857coqbot-app[bot]
2020-08-25Deprecate intro_usingGaëtan Gilbert
2020-08-25omega: stop using intro_usingGaëtan Gilbert
2020-08-25funind: stop using intro_usingGaëtan Gilbert
2020-08-25elim.ml: stop using intro_usingGaëtan Gilbert
2020-08-25Make decide equality compatible with mangled names.Gaëtan Gilbert
2020-08-25Merge PR #12758: Fixing a coercion entry transitivity bug.coqbot-app[bot]
2020-08-25Merge PR #12801: Put cyclic numbers in sort Set instead of TypeAnton Trunov
2020-08-25[test-suite] close the proofEnrico Tassi
2020-08-25added coq.vernac dependency to string_notations pluginAli Caglayan
2020-08-25Merge PR #12888: Add /dev/bench to CODEOWNERScoqbot-app[bot]
2020-08-25Merge PR #12728: Fix slow Print Universes Subgraph when many ambient universes.coqbot-app[bot]
2020-08-25added coq.vernac dependency to numeral_notations pluginAli Caglayan
2020-08-25Merge PR #12882: Perform a few tweaks to make the bench script work properly.coqbot-app[bot]
2020-08-25Merge PR #12798: Change OUnit package name to ounit2.coqbot-app[bot]
2020-08-25Merge PR #12870: CI: stop testing 4.11+trunkcoqbot-app[bot]
2020-08-25Merge PR #12778: Merging is now possible with coqbot.coqbot-app[bot]
2020-08-25Fix slow Print Universes Subgraph when many ambient universes.Gaëtan Gilbert
2020-08-25Merge PR #12878: Update sigma instead of erasing it in `update_global_env`coqbot-app[bot]
2020-08-25Add /dev/bench to CODEOWNERSGaëtan Gilbert
2020-08-24Merge PR #12886: Fix Coqtail test directory.Gaëtan Gilbert
2020-08-24Fix Coqtail test directory.whonore
2020-08-24Put cyclic numbers in sort Set instead of TypeVincent Semeria
2020-08-24Merge PR #12868: Lint stdlib with -mangle-names #1Anton Trunov
2020-08-24Merge PR #12835: Slightly reorganising the test suite to follow its documenta...Hugo Herbelin
2020-08-24Merge PR #12565: Dnets now consider axioms as being opaque for pattern recogn...coqbot
2020-08-24Update sigma instead of erasing it in `update_global_env`Maxime Dénès
2020-08-24Bench: artifact logsGaëtan Gilbert
2020-08-24Merge PR #12738: Fix subject reduction VS cumulative inductives and function etacoqbot
2020-08-24Perform a few tweaks to make the bench script work properly.Pierre-Marie Pédrot
2020-08-24Merge PR #12864: Improve `make approve-output`Gaëtan Gilbert
2020-08-24Merge PR #12854: Mini-fix in test suite: arithmetic directory does no longer ...coqbot
2020-08-24Merge PR #12832: Introduce GitHub Action to check for conflicts in PRs.coqbot
2020-08-24Merge PR #12816: Fixes #12787: anomaly of tactic injection in the presence of...Pierre-Marie Pédrot
2020-08-24CI: stop testing 4.11+trunkGaëtan Gilbert
2020-08-24added numeral_notation to META.coq.inAli Caglayan
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:05:06 +0000