diff options
| author | Hugo Herbelin | 2020-04-21 10:44:20 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-07 11:26:41 +0200 |
| commit | 3dbf278cb2fb0dae8cedf261388bbdaeff656a88 (patch) | |
| tree | bd374e3c02eb143fa4161cbcbb04ac839de8ff32 /doc | |
| parent | dd9bcf341e40b53710dc42b3cb49aed796612631 (diff) | |
Adding change log for #12146.
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/04-tactics/12146-master+fix10812-subst-failure-section-variables.rst | 9 |
1 files changed, 9 insertions, 0 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 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 <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>`_). |