From dd9bcf341e40b53710dc42b3cb49aed796612631 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 21 Apr 2020 11:48:01 +0200
Subject: 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".
---
 test-suite/bugs/closed/bug_10812.v | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_10812.v

(limited to 'test-suite')

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.
-- 
cgit v1.2.3