From 8aebd0c751db55c0301518d8ed55b8ac7bccae27 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 15 May 2015 11:31:16 +0200
Subject: Turning "Set Regular Subst Tactic" on by default (for 8.6).

---
 test-suite/success/subst.v | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)
 create mode 100644 test-suite/success/subst.v

(limited to 'test-suite')

diff --git a/test-suite/success/subst.v b/test-suite/success/subst.v
new file mode 100644
index 0000000000..8336f6a806
--- /dev/null
+++ b/test-suite/success/subst.v
@@ -0,0 +1,25 @@
+(* Test various subtleties of the "subst" tactics *)
+
+(* Should proceed from left to right (see #4222) *)
+Goal forall x y, x = y -> x = 3 -> y = 2 -> x = y.
+intros.
+subst.
+change (3 = 2) in H1.
+change (3 = 3).
+Abort.
+
+(* Should work with "x = y" and "x = t" equations (see #4214, failed in 8.4) *)
+Goal forall x y, x = y -> x = 3 -> x = y.
+intros.
+subst.
+change (3 = 3).
+Abort.
+
+(* Should substitute cycles once, until a recursive equation is obtained *)
+(* (failed in 8.4) *)
+Goal forall x y, x = S y -> y = S x -> x = y.
+intros.
+subst.
+change (y = S (S y)) in H0.
+change (S y = y).
+Abort.
-- 
cgit v1.2.3