aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
2020-09-17Formally deprecate the double induction tactic.Pierre-Marie Pédrot
The doc states it is deprecated since 1386cd9 but this was ages before the deprecation mechanism existed.
2020-09-11Rename Numeral Notation command to Number NotationPierre Roux
Keep Numeral Notation wit a deprecation warning.
2020-09-09Merge PR #12094: Extend app_inj_tail and other list lemmasHugo Herbelin
Reviewed-by: anton-trunov Ack-by: herbelin
2020-09-09Merge PR #12905: Lint stdlib with -mangle-names #2coqbot-app[bot]
Reviewed-by: anton-trunov Ack-by: jashug Ack-by: olaure01
2020-09-07Add iff variants for other list lemmasEdward Wang
2020-09-07Add iff variant for app_inj_tailEdward Wang
The lemma is true in the other direction and can be useful in proofs.
2020-08-27Merge PR #12913: Modify lia to work with -mangle-namescoqbot-app[bot]
Reviewed-by: maximedenes Ack-by: SkySkimmer
2020-08-27Merge PR #12898: [ssr] backport ssrbool from Math Comp 1.11Enrico Tassi
Ack-by: chdoc Reviewed-by: gares
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-26address comments and fixupsReynald Affeldt
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-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-25fix notation-incompatible-format warningsReynald Affeldt
(mathcomp commit 1bbfe3429a07bee2478fd15adf45b982fdfb5d2b)
2020-08-25Merge PR #12801: Put cyclic numbers in sort Set instead of TypeAnton Trunov
Ack-by: Zimmi48 Reviewed-by: anton-trunov
2020-08-25add contra lemmas introduced by MathComp's PR #499Reynald Affeldt
(https://github.com/math-comp/math-comp/pull/499/)
2020-08-25tentative backport of ssrbool from MathComp 1.11Reynald Affeldt
2020-08-24Put cyclic numbers in sort Set instead of TypeVincent Semeria
Added user overlay for bignums
2020-08-20Modify Init/Specif.v to compile with -mangle-namesJasper Hugunin
2020-08-20Modify Init/Datatypes.v to compile with -mangle-names.Jasper Hugunin
All except `pair_equal_spec` completely addressed by moving dependent hypotheses before the colon.
2020-08-20Modify Init/Logic.v to compile with -mangle-names.Jasper Hugunin
This is related to coq/coq#6781. Most issues are with `destruct H` where H is the name of a binder in the goal; this is addressed by moving dependent assumptions before the colon. A different option would be adding `intros` tactics, but this repeats the names of hypotheses (in the type of the goal and in the proof script). Additionally, the `destruct H with (Q:=...)` form gets changed to `destruct (H ...)`, since the binder name `Q` is refreshed.
2020-08-13Merge PR #12799: [stdlib] [List] Additional statements about List.repeatAnton Trunov
Reviewed-by: anton-trunov
2020-08-13Merge PR #12716: deprecate prod_curry and prod_uncurryAnton Trunov
Reviewed-by: anton-trunov
2020-08-13Merge PR #12556: Bring Float notations in line with stdlibHugo Herbelin
Reviewed-by: erikmd Reviewed-by: herbelin
2020-08-12Additional statements about List.repeatOlivier Laurent
Co-authored-by: Anton Trunov <anton.a.trunov@gmail.com>
2020-08-11deprecate prod_curry and prod_uncurryYishuai Li
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-23 19:27:24 +0000