aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-08-27Merge PR #12862: [coqchk] Look inside inner modules as wellPierre-Marie Pédrot
2020-08-27Merge PR #12918: tacinterp mini cleanup useless letinPierre-Marie Pédrot
2020-08-27Merge PR #12499: Clean future goalsPierre-Marie Pédrot
2020-08-27Merge PR #12913: Modify lia to work with -mangle-namescoqbot-app[bot]
2020-08-27Merge PR #12850: Avoid running configure when plugins/ modifiedcoqbot-app[bot]
2020-08-27Merge PR #12877: Propagate in-context information for explicitation of extra ...coqbot-app[bot]
2020-08-27Merge PR #12867: Fast freeze summarycoqbot-app[bot]
2020-08-27Merge PR #12911: Use the lite variants of performance tests in the bench defa...coqbot-app[bot]
2020-08-27tacinterp mini cleanup useless letinGaëtan Gilbert
2020-08-27Merge PR #12898: [ssr] backport ssrbool from Math Comp 1.11Enrico Tassi
2020-08-26Merge PR #12085: Convert ltac2 chapter to use prodn, update syntaxcoqbot-app[bot]
2020-08-26Modify lia to work with -mangle-namesJasper Hugunin
2020-08-26Wrap future goals into a moduleMaxime Dénès
2020-08-26Add test for #10939Maxime Dénès
2020-08-26Make future_goals stack explicit in the evarmapMaxime Dénès
2020-08-26Move given_up goals to evar_mapMaxime Dénès
2020-08-26Better encapsulation of future goalsMaxime Dénès
2020-08-26Use the lite variants of performance tests in the bench default packages.Pierre-Marie Pédrot
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-26address comments and fixupsReynald Affeldt
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-25Convert ltac2 chapter to use prodn, update syntaxJim Fehrle
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-25fix notation-incompatible-format warningsReynald Affeldt
2020-08-25The body of a let is considered to be "in context" if its type is present.Hugo Herbelin
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-25Propagate in-context information for extra arguments of notations too.Hugo Herbelin
2020-08-25Dead code in adjust_implicit_arguments.Hugo Herbelin
2020-08-25added coq.vernac dependency to numeral_notations pluginAli Caglayan
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 06:41:07 +0000