From 0d90ab680abd1f558f1c20b79b66ca6b71864fbf Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 19 Sep 2014 10:23:46 +0200
Subject: Fixing #3641 (loop in e_contextually, introduced in r16525).

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

(limited to 'test-suite')

diff --git a/test-suite/success/change.v b/test-suite/success/change.v
index 7bed7ecb15..f775f818ab 100644
--- a/test-suite/success/change.v
+++ b/test-suite/success/change.v
@@ -38,3 +38,10 @@ Fail change True with (let (x,a) := ex_intro _ True (eq_refl True) in x).
 Fail change True with
         match ex_intro _ True (eq_refl True) with ex_intro x _ => x end.
 Abort.
+
+(* Check absence of loop in identity substitution (was failing up to
+   Sep 2014, see #3641) *)
+
+Goal True.
+change ?x with x.
+Abort.
-- 
cgit v1.2.3