From 24d5448c65ba05072a5ab4180c9be95670ce126d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 30 Sep 2016 18:59:11 +0200
Subject: More tests for tactic "subst".

---
 test-suite/success/subst.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/subst.v b/test-suite/success/subst.v
index 8336f6a806..25ee81b587 100644
--- a/test-suite/success/subst.v
+++ b/test-suite/success/subst.v
@@ -23,3 +23,20 @@ subst.
 change (y = S (S y)) in H0.
 change (S y = y).
 Abort.
+
+(* A bug revealed by OCaml 4.03 warnings *)
+(* fixes in 4e3d464 and 89ec88f for v8.5, 4e3d4646 and 89ec88f1e for v8.6 *)
+Goal forall y, let x:=0 in y=x -> y=y.
+intros * H;
+(* This worked as expected *)
+subst.
+Fail clear H.
+Abort.
+
+Goal forall y, let x:=0 in x=y -> y=y.
+intros * H;
+(* Before the fix, this unfolded x instead of 
+   substituting y and erasing H *)
+subst.
+Fail clear H.
+Abort.
-- 
cgit v1.2.3