aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog/04-tactics
AgeCommit message (Collapse)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
The old code was generating different patterns, depending on whether a projection with parameters was expanded or not. In the first case, parameters were present, whereas in the latter they were not. We fix this by adding dummy parameter arguments on sight. Fixes #14009: TC search failure with primitive projections.
2021-03-26Fix Ltac2 `Array.init` exponential overheadJason Gross
Previously, `Array.init` was computing the first element of the array twice, resulting in exponential overhead in the number of recursive nestings of `Array.init`. Notably, since `Array.map` is implemented in terms of `Array.init`, this exponential blowup shows up in any term traversal based on `Array.map` over the arguments of application nodes. Fixes #14011
2021-03-04Fix #12011 ssreflect "rewrite in" with setoidsGaëtan Gilbert
ssreflect asks setoid rewrite to rewrite in goal "forall_special_name_ : T, _other_name_" Since this is a non dependent product, setoid rewrite converts that to "impl T _other_name_" and must be taught to restore the special name when unfolding impl.
2021-01-28Merge PR #13781: [micromega] Deprecate hopefully useless options and flagscoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: jfehrle
2021-01-25Update doc/changelog/04-tactics/13781-deprecate_micromega_options.rstFrédéric Besson
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2021-01-24Merge PR #13762: Remove double induction tacticPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2021-01-22changelogBESSON Frederic
2021-01-22Merge PR #13761: Remove convert_concl_no_check (deprecated in 8.11)Pierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ppedrot
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
Ack-by: SkySkimmer Reviewed-by: ppedrot
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
at ..." instead) Ack-by: Zimmi48 Reviewed-by: ppedrot
2021-01-06[micromega] Add missing support for `implb`BESSON Frederic
2021-01-02Deprecate "at ... with ..." in change tacticJim Fehrle
(use "with ... at ..." instead)
2020-12-16Merge PR #13568: Fix #13566: Add checks for invalid occurrences in several ↵Pierre-Marie Pédrot
tactics. Reviewed-by: ppedrot
2020-12-14Adding change log for #13568.Hugo Herbelin
2020-12-13Add changelog for #13509.Hugo Herbelin
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
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
This reverts commit f3642ad8bdf6d9aa1b411892e5e6815a6a75e4d5.
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 ↵coqbot-app[bot]
sense Reviewed-by: Zimmi48
2020-11-21Merge PR #12246: Adding support for applying in several hypotheses at the ↵Pierre-Marie Pédrot
same time (granting #9816) Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-11-20Merge PR #13237: Address #13235: avoid passing degenerate in-hyps clausesPierre-Marie Pédrot
Reviewed-by: jfehrle Reviewed-by: ppedrot
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]
Reviewed-by: Zimmi48 Reviewed-by: herbelin
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 ↵coqbot-app[bot]
of the definition of the metas Reviewed-by: mattam82
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
Update doc/sphinx/addendum/micromega.rst Co-authored-by: Jason Gross <jasongross9@gmail.com> Update theories/micromega/ZifyInt63.v Co-authored-by: Jason Gross <jasongross9@gmail.com>
2020-09-23Merge PR #12847: Tactics inversion and replace work with eq in typePierre-Marie Pédrot
Reviewed-by: ppedrot
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
Fixes #12571.
2020-06-20Add a pre-hook mechanism for the `zify` tacticKazuhiko Sakaguchi
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-20 09:15:04 +0000