aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
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-25ring: generate fresh names for lemmasGaëtan Gilbert
Fix #12889
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 14:12:28 +0000