From 3dbf278cb2fb0dae8cedf261388bbdaeff656a88 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 21 Apr 2020 10:44:20 +0200 Subject: Adding change log for #12146. Co-Authored-By: Théo Zimmermann --- .../12146-master+fix10812-subst-failure-section-variables.rst | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 doc/changelog/04-tactics/12146-master+fix10812-subst-failure-section-variables.rst 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 new file mode 100644 index 0000000000..055006d3b4 --- /dev/null +++ b/doc/changelog/04-tactics/12146-master+fix10812-subst-failure-section-variables.rst @@ -0,0 +1,9 @@ +- **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 `_, + by Hugo Herbelin; fixes `#10812 `_; + fixes `#12139 `_). -- cgit v1.2.3