aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog/04-tactics
AgeCommit message (Expand)Author
2021-04-19changelog entry for Ltac2 unifySamuel Gruetter
2021-04-02Remove the omega tactic and related optionsJim Fehrle
2021-04-01changelog for 8.13.2Enrico Tassi
2021-03-30Properly expand projection parameters in Btermdn.Pierre-Marie Pédrot
2021-03-26Fix Ltac2 `Array.init` exponential overheadJason Gross
2021-03-04Fix #12011 ssreflect "rewrite in" with setoidsGaëtan Gilbert
2021-01-28Merge PR #13781: [micromega] Deprecate hopefully useless options and flagscoqbot-app[bot]
2021-01-25Update doc/changelog/04-tactics/13781-deprecate_micromega_options.rstFrédéric Besson
2021-01-24Merge PR #13762: Remove double induction tacticPierre-Marie Pédrot
2021-01-22changelogBESSON Frederic
2021-01-22Merge PR #13761: Remove convert_concl_no_check (deprecated in 8.11)Pierre-Marie Pédrot
2021-01-20Remove double induction tacticJim Fehrle
2021-01-19Remove convert_concl_no_checkJim Fehrle
2021-01-19Merge PR #13699: Fix #13579 (hnf on primitives raises an anomaly)Pierre-Marie Pédrot
2021-01-18Adding changelog for #13512.Hugo Herbelin
2021-01-18Add changelogPierre Roux
2021-01-07Use nat_or_var for fail/gfailJim Fehrle
2021-01-07Merge PR #13696: Deprecate "at ... with ..." in change tactic (use "with ... ...Pierre-Marie Pédrot
2021-01-06[micromega] Add missing support for `implb`BESSON Frederic
2021-01-02Deprecate "at ... with ..." in change tacticJim Fehrle
2020-12-16Merge PR #13568: Fix #13566: Add checks for invalid occurrences in several ta...Pierre-Marie Pédrot
2020-12-14Adding change log for #13568.Hugo Herbelin
2020-12-13Add changelog for #13509.Hugo Herbelin
2020-12-03[changelog] update markupEnrico Tassi
2020-12-03Changes for Coq 8.13Matthieu Sozeau
2020-11-27Revert "Remove deprecated tactic cutrewrite."Théo Zimmermann
2020-11-24Convert auto chapter to prodnJim Fehrle
2020-11-23Merge PR #13417: Use nat_or_var in grammar where negative values don't make s...coqbot-app[bot]
2020-11-21Merge PR #12246: Adding support for applying in several hypotheses at the sam...Pierre-Marie Pédrot
2020-11-20Merge PR #13237: Address #13235: avoid passing degenerate in-hyps clausesPierre-Marie Pédrot
2020-11-20Use nat_or_var where negative values don't make senseJim Fehrle
2020-11-20Adding change log.Hugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:55:42 +0000