aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog/04-tactics
AgeCommit message (Expand)Author
2020-09-23Merge PR #12847: Tactics inversion and replace work with eq in typePierre-Marie Pédrot
2020-09-08Remove deprecated tactic cutrewrite.Théo Zimmermann
2020-08-20Adding change log for PR #12816.Hugo Herbelin
2020-08-18Adding change log for #12847.Hugo Herbelin
2020-07-23[changelog] Latest changes backported to 8.12 branch.Emilio Jesus Gallego Arias
2020-06-23Correctly classify variables as being unfoldable in dnet patterns.Pierre-Marie Pédrot
2020-06-20Add a pre-hook mechanism for the `zify` tacticKazuhiko Sakaguchi
2020-06-14[micromega] native support for boolean operatorsFrédéric Besson
2020-06-11Merge PR #12423: Remove info tactic, deprecated in 8.5Pierre-Marie Pédrot
2020-06-01Merge PR #12396: Release notes 8.12Emilio Jesus Gallego Arias
2020-05-30Remove info tactic, deprecated in 8.5Jim Fehrle
2020-05-28Merge PR #12399: Remove the prolog tactic.Théo Zimmermann
2020-05-27Add more changelog entries which have been backported to v8.12.Théo Zimmermann
2020-05-27Release notes for 8.12.Théo Zimmermann
2020-05-25Add a changelog.Pierre-Marie Pédrot
2020-05-19Delay evaluating arguments of the "exists" tacticAttila Gáspár
2020-05-16Fix #11761: Functional Induction throws unrecoverable error.Pierre Courtieu
2020-05-14Merge PR #12256: Move the static check of evaluability in unfold tactic to ru...Hugo Herbelin
2020-05-14Add a changelog for 8.11.2.Pierre-Marie Pédrot
2020-05-14Adding changelog.Pierre-Marie Pédrot
2020-05-12Merge PR #12223: Locating error again in atomic tactics (fixes #12152)Pierre-Marie Pédrot
2020-05-12Merge PR #12146: Fixes #10812: tactic subst failure with section variables in...Pierre-Marie Pédrot
2020-05-10Change log for #12223.Hugo Herbelin
2020-05-09Add a `with_strategy` tacticJason Gross
2020-05-07Adding change log for #12146.Hugo Herbelin
2020-04-30[zify] add support for Nat.le, Nat.lt and Nat.eqFrédéric Besson
2020-04-21Change log for #12023Hugo Herbelin
2020-04-21Merge PR #12116: Fixing #12045: missing normalization in conclusion of custom...Pierre-Marie Pédrot
2020-04-21Merge PR #11883: Fix #7812: autounfold's behavior depends on file namesHugo Herbelin
2020-04-20Change log for PR #12045.Hugo Herbelin
2020-04-17Deprecate “omega”Vincent Laporte
2020-04-16NativeCompute Timing: Use real, not user timeJason Gross
2020-04-11Fix #7812Attila Gáspár
2020-03-30Merge PR #11018: “auto with zarith”: use “lia” rather than “omega”Maxime Dénès
2020-03-26Change logHugo Herbelin
2020-03-24“auto with zarith”: use “lia” rather than “omega”Vincent Laporte
2020-03-21Add module ZifyPow to avoid compatibility issue with 8.11.Théo Zimmermann
2020-03-19firstorder: default tactic is “auto with core”Vincent Laporte
2020-03-08Minor improvements to the unreleased changelog.Théo Zimmermann
2020-03-05Merge PR #11522: Adding an alias `pose proof (x:=t)` for `pose proof t as x` ...Pierre-Marie Pédrot
2020-03-03[zify] efficiency improvementsFrédéric Besson
2020-03-03Update doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rstHugo Herbelin
2020-03-03Adding an alias "pose proof (x:=a)" for "pose proof a as x".Hugo Herbelin
2020-02-13Merge PR #11441: Add explicit types to changelog entries that were still miss...Emilio Jesus Gallego Arias
2020-02-03Fix efficiency regression #11436Frédéric Besson
2020-01-25Merge PR #11025: Add Set NativeCompute TimingMaxime Dénès
2020-01-22Add explicit types to changelog entries.Théo Zimmermann
2020-01-22Changelog for 8.11.0.Théo Zimmermann
2020-01-17Merge PR #11362: Lia bugfix 11191Maxime Dénès
2020-01-14[zify] elim let in MLFrédéric Besson
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 22:31:56 +0000