aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog/04-tactics
AgeCommit message (Expand)Author
2020-11-20Merge PR #13237: Address #13235: avoid passing degenerate in-hyps clausesPierre-Marie Pédrot
2020-11-20Merge PR #13403: Use only nats for occs_nums rather than intscoqbot-app[bot]
2020-11-19Adding changelog for #13237.Hugo Herbelin
2020-11-19[changelog] Indicate a replacement for deprecated syntax of debug / info_eauto.Théo Zimmermann
2020-11-18Use only nats for occs_nums rather than intsJim Fehrle
2020-11-16Add changelog for #13337.Hugo Herbelin
2020-11-16Merge PR #13373: Fixes #13363: in pose_all_metas_as_evars, use the context of...coqbot-app[bot]
2020-11-16Slight improvement to the changelog entry.Théo Zimmermann
2020-11-15Deprecate "eauto @int_or_var @int_or_var", add "bfs eauto"Jim Fehrle
2020-11-13Add changelog for #13373.Hugo Herbelin
2020-11-05Changelog for 8.12.1.Théo Zimmermann
2020-10-20[zify] Add support for Int63.intFrédéric Besson
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-25 00:05:48 +0000