Skip to content

Commit

Permalink
Adding change log for coq#12146.
Browse files Browse the repository at this point in the history
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
  • Loading branch information
herbelin and Zimmi48 committed May 3, 2020
1 parent daba99e commit 159fa8a
Showing 1 changed file with 9 additions and 0 deletions.
@@ -0,0 +1,9 @@
- **Changed:**
Tactic :tacn:`subst @id` 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`
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>`_).

0 comments on commit 159fa8a

Please sign in to comment.