aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Expand)Author
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
2020-07-23Merge PR #12679: Remove redundant data from VM case switch.Gaëtan Gilbert
2020-07-23Merge PR #12698: Fixing mention of `unfold` as example of tactic taking a qua...Théo Zimmermann
2020-07-22Remove redundant data from VM case switch.Pierre-Marie Pédrot
2020-07-21Turn various anomalies into regular errors in primitive declaration pathGaëtan Gilbert
2020-07-17Add tests for the interpretation of "unfold".Hugo Herbelin
2020-07-11Merge PR #12646: Correctly readback blocked CaseInvert matches in VM/nativePierre-Marie Pédrot
2020-07-09Add test for #10890 derive vs abstractGaëtan Gilbert
2020-07-06Correctly readback blocked CaseInvert matches in VM/nativeGaëtan Gilbert
2020-07-01UIP in SPropGaëtan Gilbert
2020-06-29[test-suite] async-proofs off in tests with Fail TimeoutEnrico Tassi
2020-05-18Update to 8.13.Théo Zimmermann
2020-05-16Fix #11761: Functional Induction throws unrecoverable error.Pierre Courtieu
2020-05-15Merge PR #11992: do not re-export ListNotations from ProgramAnton Trunov
2020-05-14Move the static check of evaluability in unfold tactic to runtime.Pierre-Marie Pédrot
2020-05-13Merge PR #11828: [obligations] Deprecated flag cleanupGaëtan Gilbert
2020-05-11Merge PR #12254: In non-strict mode, accept any variable as a tactic reference.Hugo Herbelin
2020-05-09Revert "[with_strategy] Fix for coqchk"Jason Gross
2020-05-09Fix a bug with with_strategy, behavior on multisuccess tacticsJason Gross
2020-05-09Elaborate with_strategy warningJason Gross
2020-05-09Fix the `with_strategy` tactic to work with `abstract`Jason Gross
2020-05-09Add a `with_strategy` tacticJason Gross
2020-05-08In non-strict mode, accept any variable as a tactic reference.Pierre-Marie Pédrot
2020-05-02LtacProf now handles multi-success backtrackingJason Gross
2020-04-30do not re-export ListNotations from Program: fix testsuiteAntonio Nikishaev
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-19 08:11:26 +0000