aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Collapse)Author
2021-04-23Merge PR #14041: Enable canonical fun _ => _ projections.coqbot-app[bot]
Reviewed-by: gares Ack-by: Janno Ack-by: CohenCyril Ack-by: Zimmi48 Ack-by: jfehrle Ack-by: SkySkimmer
2021-04-22Enable canonical `fun _ => _` projections.Jan-Oliver Kaiser
2021-04-14Merge PR #14050: Remove remote counter systemcoqbot-app[bot]
Reviewed-by: gares Ack-by: ppedrot Ack-by: ejgallego
2021-04-14Remove remote counter systemGaëtan Gilbert
2021-04-12[zify] More aggressive application of saturation rulesBESSON Frederic
The role of the `zify_saturate` tactic is to augment the goal with positivity constraints. The premisses were previously obtained from the context. If they are not present, we instantiate the saturation lemma anyway. Also, - Remove saturation rules for Z.mul, the reasoning is performed by lia/nia - Run zify_saturate after zify_to_euclidean_division_equations - Better lemma for Z.power - Ensure that lemma are generated once Co-authored-by: Andrej Dudenhefner <mrhaandi> Closes #12184, #11656
2021-04-02Remove the omega tactic and related optionsJim Fehrle
2021-01-20Remove double induction tacticJim Fehrle
2021-01-19Merge PR #13512: Fixes #13413: freshness failure in apply-in introduction ↵Pierre-Marie Pédrot
pattern Reviewed-by: ppedrot
2021-01-18Preventing internal temporary names to impact the "?H"-like intro-pattern names.Hugo Herbelin
2021-01-18Fixes #13413: freshness issue with "%" introduction pattern.Hugo Herbelin
We build earlier the final expected name at the end of a sequence of "%" introduction patterns.
2021-01-18Support locality attributes for Hint Rewrite (including export)Gaëtan Gilbert
We deprecate unspecified locality as was done for Hint. Close #13724
2021-01-12Add a test for bound variables in match goal over a case involving variables.Pierre-Marie Pédrot
2021-01-11Add a test for a weird behaviour of tactic matching.Pierre-Marie Pédrot
The arity of a destructuring let in a pattern is allowed to be shorter than the case term node it actually matches. This is an unexpected side-effect of the legacy expanded representation of cases that happens to be relied upon in the wild, as evidenced by the CI failures from #13723.
2021-01-07Merge PR #13696: Deprecate "at ... with ..." in change tactic (use "with ... ↵Pierre-Marie Pédrot
at ..." instead) Ack-by: Zimmi48 Reviewed-by: ppedrot
2021-01-02Deprecate "at ... with ..." in change tacticJim Fehrle
(use "with ... at ..." instead)
2020-12-31Adding a test for conversion involving let-bindings in inductive parameters.Pierre-Marie Pédrot
2020-12-31Add a test for a complex conversion involving pattern-matching with ↵Pierre-Marie Pédrot
let-bindings.
2020-12-17Add a test for change over case nodes.Pierre-Marie Pédrot
This is extracted from #13563.
2020-12-14Add checks for invalid occurrences in setoid rewrite.Hugo Herbelin
We additionally check that occurrence 0 is invalid in simpl at, unfold at, etc.
2020-12-09Fixing support for argument scopes and let-ins while interning cases patterns.Hugo Herbelin
We also simplify the whole process of interpretation of cases pattern on the way.
2020-12-08Add a test for cbv over inductive types which feature let-bindings.Pierre-Marie Pédrot
2020-11-27Merge PR #12586: [declare] Allow custom typing flags when declaring constants.coqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: gares Reviewed-by: herbelin Ack-by: jfehrle
2020-11-27Merge PR #13457: [RM] Update magicno & compatcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-26[attributes] [typing] Rename `typing` to `bypass_check`Emilio Jesus Gallego Arias
As discussed in the Coq meeting.
2020-11-26[attributes] [doc] Documentation review by Théo.Emilio Jesus Gallego Arias
Co-authored-by: <Théo Zimmermann <theo.zimmermann@inria.fr>
2020-11-26[proofs] Support per-definition typing-flags in interactive proofs.Emilio Jesus Gallego Arias
Most cases should be accounted in proof code, however be wary of paths where `Global.env ()` is used.
2020-11-26[vernac] Allow to control typing flags with attributes.Emilio Jesus Gallego Arias
The syntax is the one of boolean attributes, that is to say `#[typing($flag={yes,no}]` where `$flag` is one of `guarded`, `universes`, `positive`. We had to instrument the pretyper in a few places, it is interesting that it is doing so many checks.
2020-11-24Add a new evar source to refer to evars which are types of evars.Hugo Herbelin
To tie the knot (since the evar depends on the evar type and the source of the evar type of the evar), we use an "update_source" function. An alternative could be to provide a function to build both an evar with its evar type directly in evd.ml...
2020-11-23Update compat infrastructure for 8.14Enrico Tassi
2020-11-20Granting #9816: apply in takes several hypotheses.Hugo Herbelin
2020-11-18[attributes] Deprecate `attr(true)` syntax in favor of booelan attributes.Emilio Jesus Gallego Arias
We introduce a warning so boolean attributes are expected to be of the form `attr={yes,no}` or just `attr` (for `yes`). We update the documentation, test-suite, and changelog.
2020-11-17Merge PR #12653: Syntax for specifying cumulative inductivescoqbot-app[bot]
Reviewed-by: mattam82 Reviewed-by: maximedenes Reviewed-by: jfehrle Ack-by: gares Ack-by: Zimmi48 Ack-by: ppedrot
2020-11-16Syntax for specifying cumulative inductivesGaëtan Gilbert
2020-11-15Propagating scope information in indirect application to a reference.Hugo Herbelin
This allows the following to interpret "0" in the expected scope: Notation "0" := true : bool_scope. Axiom f : bool -> bool -> nat. Record R := { p : bool -> nat }. Check (@f 0) 0. Check fun r => r.(@p) 0.
2020-11-12Test case for Proof using in -noinit mode.Théo Zimmermann
2020-11-09[compat] remove 8.10Enrico Tassi
2020-11-06Merge PR #13284: Fixing interpretation of rewrite_strat argument in LtacPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-11-05Merge PR #12218: Numeral notations for non inductive typescoqbot-app[bot]
Reviewed-by: herbelin Reviewed-by: JasonGross Reviewed-by: jfehrle Ack-by: Zimmi48
2020-11-05Merge PR #13182: Check types when converting irrelevant terms in old unificationcoqbot-app[bot]
Reviewed-by: gares
2020-11-02[stm] support #[using] attributeEnrico Tassi
2020-11-02attribute #[using] for Definition and FixpointEnrico Tassi
2020-10-30Renaming Numeral.v into Number.vPierre Roux
2020-10-29Fixing interpretation of rewrite_strat argument in Ltac.Hugo Herbelin
Ltac variables were not yet supported.
2020-10-19Merge PR #13166: Fixes #13165: implicit arguments in defined fields of ↵coqbot-app[bot]
record types not taken into account Reviewed-by: SkySkimmer
2020-10-16Use list notation in nsatz examples referenced in the docJim Fehrle
2020-10-16Fixes/enhancements with local definitions in records.Hugo Herbelin
Fixes implicit arguments from the body of a defined field not taken into account. Get (a bit) more information for detection of SProp relevance in implicitly-typed defined field. (It should be done at the very end of the inference phase, though, because some evars may not yet be instantiated.)
2020-10-12Check types when converting irrelevant terms in old unificationGaëtan Gilbert
Fixes probably many strange issues such as the example in #13171
2020-10-09Minimize Prop <= i to i := SetGaëtan Gilbert
Fix part of #8196, fix #12414 Replaces #9343
2020-09-23Merge PR #12847: Tactics inversion and replace work with eq in typePierre-Marie Pédrot
Reviewed-by: ppedrot
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:17:22 +0000