Tactic subst now inactive on section variables occurring indirectly in goal.

This is saner behavior making subst reversible, as discussed in #12139.
This also fixes #10812 and #12139.

In passing, we also simplify a bit the code of "subst_all".

1 files changed, 28 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_10812.v b/test-suite/bugs/closed/bug_10812.v
new file mode 100644
index 0000000000..68f3814781
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10812.v
@@ -0,0 +1,28 @@
+(* subst with indirectly dependent section variables *)
+
+Section A.
+
+Variable a:nat.
+Definition b := a.
+
+Goal a=1 -> a+a=1 -> b=1.
+intros.
+Fail subst a. (* was working; we make it failing *)
+rewrite H in H0.
+discriminate.
+Qed.
+
+Goal a=1 -> a+a=1 -> b=1.
+intros.
+subst. (* should not apply to a *)
+rewrite H in H0.
+discriminate.
+Qed.
+
+Goal forall t, a=t -> b=t.
+intros.
+subst.
+reflexivity.
+Qed.
+
+End A.