aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-08-27Merge PR #12849: Rename VM-related kernel/cfoo files to kernel/vmfooPierre-Marie Pédrot
Reviewed-by: gares Reviewed-by: ppedrot Reviewed-by: silene
2020-08-27Merge PR #12862: [coqchk] Look inside inner modules as wellPierre-Marie Pédrot
Reviewed-by: ppedrot Reviewed-by: proux01
2020-08-27Merge PR #12918: tacinterp mini cleanup useless letinPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-08-27Merge PR #12499: Clean future goalsPierre-Marie Pédrot
Ack-by: SkySkimmer Ack-by: ejgallego Reviewed-by: mattam82 Reviewed-by: ppedrot
2020-08-27Merge PR #12913: Modify lia to work with -mangle-namescoqbot-app[bot]
Reviewed-by: maximedenes Ack-by: SkySkimmer
2020-08-27Merge PR #12850: Avoid running configure when plugins/ modifiedcoqbot-app[bot]
Reviewed-by: ejgallego Reviewed-by: gares
2020-08-27Merge PR #12877: Propagate in-context information for explicitation of extra ↵coqbot-app[bot]
arguments of notations Reviewed-by: SkySkimmer Ack-by: herbelin
2020-08-27Merge PR #12867: Fast freeze summarycoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-08-27Merge PR #12911: Use the lite variants of performance tests in the bench ↵coqbot-app[bot]
default packages Reviewed-by: JasonGross
2020-08-27tacinterp mini cleanup useless letinGaëtan Gilbert
2020-08-27Merge PR #12898: [ssr] backport ssrbool from Math Comp 1.11Enrico Tassi
Ack-by: chdoc Reviewed-by: gares
2020-08-26Merge PR #12085: Convert ltac2 chapter to use prodn, update syntaxcoqbot-app[bot]
Reviewed-by: JasonGross Reviewed-by: Zimmi48 Ack-by: jfehrle Ack-by: ppedrot
2020-08-26Modify lia to work with -mangle-namesJasper Hugunin
We used to be refreshing the names for intros but not using the refreshed names. The same pattern of `intro_using` (which is what `intros ?name` effectively is) messing things up as in coq/coq#12881.
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
We try to encapsulate the future goals abstraction in the evar map. A few calls to `save_future_goals` and `restore_future_goals` are still there, but we try to minimize them. This is a preliminary refactoring to make the invariants between the shelf and future goals more explicit, before giving unification access to the shelf, which is needed for #7825.
2020-08-26Use the lite variants of performance tests in the bench default packages.Pierre-Marie Pédrot
They are much faster and should be as informative as their heavy counterparts. I have been forgetting to do that for a long time already.
2020-08-26Merge PR #12764: A fix and two enhancements of trailing pattern ↵Pierre-Marie Pédrot
factorization in recursive notations Reviewed-by: ppedrot
2020-08-26Merge PR #12904: Move bench job definition to its own filePierre-Marie Pédrot
Reviewed-by: ppedrot
2020-08-26Merge PR #12881: Deprecate intro_usingPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-08-26Merge PR #12901: [bench] Remove useless commit guessing logicPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-08-26Merge PR #12884: Documentation of coq_makefile: fix name of installation dir ↵coqbot-app[bot]
+ help on using option -f Reviewed-by: jfehrle Ack-by: herbelin
2020-08-26Merge PR #12861: Require NsatzTactic: nsatz support for Z and QPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: jfehrle Reviewed-by: ppedrot Reviewed-by: thery
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
Add a mli file and uniformize indentation on the way.
2020-08-25A fix and two enhancements of trailing pattern factorization in rec. notations.Hugo Herbelin
The fix is a missing check of equality of custom entries. The enhancements are: - not to bother breaking hints - not to care about the border or internal position when the level is made explicit Ideally, one could also improve the treatment of DefaultLevel. To be done later on.
2020-08-25Move bench job definition to its own fileGaëtan Gilbert
This focuses review requests to bench-maintainers instead of sharing with ci-maintainers
2020-08-25Require NsatzTactic: nsatz support for Z and QJason Gross
The purpose of `NsatzTactic` is to allow using `nsatz` without the dependency on real axioms. So we declare the instances for `Z` and `Q` in that file, so that users don't have to re-create them. Fixes #12860
2020-08-25Remove useless commit guessing logicJason Gross
On GitLab, we don't need to base the job info on the PR number, since it ought to be available from the git repo. Removing the logic will make the bench infrastructure more uniform.
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]
Reviewed-by: ejgallego Ack-by: Alizter Ack-by: gares
2020-08-25Merge PR #12897: [test-suite] close the proof added in #12857coqbot-app[bot]
Reviewed-by: Zimmi48
2020-08-25Deprecate intro_usingGaëtan Gilbert
This is a footgun as it can refresh the name. Callers can still ignore the generated name by doing `intro_using_then id (fun _ -> tclUNIT())`.
2020-08-25omega: stop using intro_usingGaëtan Gilbert
This makes the test suite Omega.v compatible with Mangle Names Not sure how `reintroduce` works since it ignores the refreshed name, considering omega is deprecated it's not worth figuring out so long as it works (NB making it use intro_mustbe_force makes the test suite fail so it must be doing something right).
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
Fix #12676
2020-08-25fix notation-incompatible-format warningsReynald Affeldt
(mathcomp commit 1bbfe3429a07bee2478fd15adf45b982fdfb5d2b)
2020-08-25The body of a let is considered to be "in context" if its type is present.Hugo Herbelin
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-08-25Merge PR #12758: Fixing a coercion entry transitivity bug.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-08-25Merge PR #12801: Put cyclic numbers in sort Set instead of TypeAnton Trunov
Ack-by: Zimmi48 Reviewed-by: anton-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]
Reviewed-by: Zimmi48
2020-08-25Merge PR #12728: Fix slow Print Universes Subgraph when many ambient universes.coqbot-app[bot]
Reviewed-by: ejgallego
2020-08-25Propagate in-context information for extra arguments of notations too.Hugo Herbelin
2020-08-25Dead code in adjust_implicit_arguments.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 20:06:49 +0000