aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Expand)Author
2021-01-20Remove double induction tacticJim Fehrle
2021-01-19Merge PR #13512: Fixes #13413: freshness failure in apply-in introduction pat...Pierre-Marie Pédrot
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
2021-01-18Support locality attributes for Hint Rewrite (including export)Gaëtan Gilbert
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
2021-01-07Merge PR #13696: Deprecate "at ... with ..." in change tactic (use "with ... ...Pierre-Marie Pédrot
2021-01-02Deprecate "at ... with ..." in change tacticJim Fehrle
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 let-bindi...Pierre-Marie Pédrot
2020-12-17Add a test for change over case nodes.Pierre-Marie Pédrot
2020-12-14Add checks for invalid occurrences in setoid rewrite.Hugo Herbelin
2020-12-09Fixing support for argument scopes and let-ins while interning cases patterns.Hugo Herbelin
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]
2020-11-27Merge PR #13457: [RM] Update magicno & compatcoqbot-app[bot]
2020-11-26[attributes] [typing] Rename `typing` to `bypass_check`Emilio Jesus Gallego Arias
2020-11-26[attributes] [doc] Documentation review by Théo.Emilio Jesus Gallego Arias
2020-11-26[proofs] Support per-definition typing-flags in interactive proofs.Emilio Jesus Gallego Arias
2020-11-26[vernac] Allow to control typing flags with attributes.Emilio Jesus Gallego Arias
2020-11-24Add a new evar source to refer to evars which are types of evars.Hugo Herbelin
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
2020-11-17Merge PR #12653: Syntax for specifying cumulative inductivescoqbot-app[bot]
2020-11-16Syntax for specifying cumulative inductivesGaëtan Gilbert
2020-11-15Propagating scope information in indirect application to a reference.Hugo Herbelin
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
2020-11-05Merge PR #12218: Numeral notations for non inductive typescoqbot-app[bot]
2020-11-05Merge PR #13182: Check types when converting irrelevant terms in old unificationcoqbot-app[bot]
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
2020-10-19Merge PR #13166: Fixes #13165: implicit arguments in defined fields of record...coqbot-app[bot]
2020-10-16Use list notation in nsatz examples referenced in the docJim Fehrle
2020-10-16Fixes/enhancements with local definitions in records.Hugo Herbelin
2020-10-12Check types when converting irrelevant terms in old unificationGaëtan Gilbert
2020-10-09Minimize Prop <= i to i := SetGaëtan Gilbert
2020-09-23Merge PR #12847: Tactics inversion and replace work with eq in typePierre-Marie Pédrot
2020-09-17Formally deprecate the double induction tactic.Pierre-Marie Pédrot
2020-09-11Rename Numeral Notation command to Number NotationPierre Roux
2020-08-31Fixes a freshness issue with induction (see comment in #12944).Hugo Herbelin
2020-08-28Name saved goals in name_mangling testGaëtan Gilbert
2020-08-28Make abstract compatible with mangle namesGaëtan Gilbert
2020-08-19Do not refresh the names of implicit arguments.Jasper Hugunin
2020-08-18Tactic replace: adding support for registration of an equality in Type.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 00:03:53 +0000