aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-26Fix algebraic comparison with sprop on one sideGaëtan Gilbert
Close #12909
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-25Modify Numbers/NatInt/NZGcd.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZDiv.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZLog.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZSqrt.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZPow.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZParity.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZMulOrder.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZOrder.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZMul.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZAdd.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZBase.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Structures/GenericMinMax.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Structures/OrdersFacts.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Structures/OrdersTac.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Structures/Orders.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Relations/Relations.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Relations/Operators_Properties.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Setoids/Setoid.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Classes/CMorphisms.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Classes/CRelationClasses.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Classes/Morphisms.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Classes/RelationClasses.v to compile with -mangle-namesJasper Hugunin
The apply <- tactic was breaking, so we had to modify the definition in Init/Tactics.v to use slightly fresher names.
2020-08-25Modify Bool/Bool.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Init/Tactics.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Init/Wf.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Init/Peano.v to compile with -mangle-names.Jasper Hugunin
Here I added intros rather than moving premises before the colon, partly to be more consistent with nearby lemma statements.
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-25[bench] Update bench script with better urls and more infoJason Gross
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-18 02:08:09 +0000