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

Ack-by: Zimmi48
Reviewed-by: ppedrot

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.