diff options
Diffstat (limited to 'doc/changelog/04-tactics/12146-master+fix10812-subst-failure-section-variables.rst')
| -rw-r--r-- | doc/changelog/04-tactics/12146-master+fix10812-subst-failure-section-variables.rst | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/doc/changelog/04-tactics/12146-master+fix10812-subst-failure-section-variables.rst b/doc/changelog/04-tactics/12146-master+fix10812-subst-failure-section-variables.rst deleted file mode 100644 index 055006d3b4..0000000000 --- a/doc/changelog/04-tactics/12146-master+fix10812-subst-failure-section-variables.rst +++ /dev/null @@ -1,9 +0,0 @@ -- **Changed:** - Tactic :tacn:`subst` :n:`@ident` now fails over a section variable which is - indirectly dependent in the goal; the incompatibility can generally - be fixed by first clearing the hypotheses causing an indirect - dependency, as reported by the error message, or by using :tacn:`rewrite` :n:`in *` - instead; similarly, :tacn:`subst` has no more effect on such variables - (`#12146 <https://github.com/coq/coq/pull/12146>`_, - by Hugo Herbelin; fixes `#10812 <https://github.com/coq/coq/pull/10812>`_; - fixes `#12139 <https://github.com/coq/coq/pull/12139>`_). |