Merge PR #12146: Fixes #10812: tactic subst failure with section variables indirectly dependent in goal

Ack-by: Zimmi48
Reviewed-by: ppedrot

2 files changed, 27 insertions, 2 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>`_).
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index bc2168411b..439f7fb9f6 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -2832,6 +2832,11 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
    If :n:`@ident` is a local definition of the form :n:`@ident := t`, it is also
    unfolded and cleared.
 
+   If :n:`@ident` is a section variable it is expected to have no
+   indirect occurrences in the goal, i.e. that no global declarations
+   implicitly depending on the section variable must be present in the
+   goal.
+
    .. note::
       + When several hypotheses have the form :n:`@ident = t` or :n:`t = @ident`, the
         first one is used.
@@ -2845,9 +2850,11 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
 
    .. tacv:: subst
 
-      This applies subst repeatedly from top to bottom to all identifiers of the
+      This applies :tacn:`subst` repeatedly from top to bottom to all hypotheses of the
       context for which an equality of the form :n:`@ident = t` or :n:`t = @ident`
-      or :n:`@ident := t` exists, with :n:`@ident` not occurring in ``t``.
+      or :n:`@ident := t` exists, with :n:`@ident` not occurring in
+      ``t`` and :n:`@ident` not a section variable with indirect
+      dependencies in the goal.
 
    .. flag:: Regular Subst Tactic
 
@@ -2873,6 +2880,15 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
       hypotheses, which without the flag it may break.
       default.
 
+   .. exn:: Cannot find any non-recursive equality over :n:`@ident`.
+      :undocumented:
+
+   .. exn:: Section variable :n:`@ident` occurs implicitly in global declaration :n:`@qualid` present in hypothesis :n:`@ident`.
+            Section variable :n:`@ident` occurs implicitly in global declaration :n:`@qualid` present in the conclusion.
+
+      Raised when the variable is a section variable with indirect
+      dependencies in the goal.
+
 
 .. tacn:: stepl @term
    :name: stepl