From 32a9a4e3656e581af41c26f48f63ed1daec331d8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 6 May 2015 18:54:18 +0200
Subject: Fixing treatment of recursive equations damaged by 857e82b2ca0d1.
 Improving treatment of recursive equations compared to 8.4 (see test-suite).
 Experimenting not to unfold local defs ever in subst. (+ Slight
 simplification in checking reflexive equalities only once).

---
 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