From eec75e3814818ec96ac1045c2dd63e242620dcfe Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 21 Mar 2013 21:45:37 +0000
Subject: Cosmetic code contraction in evarsolve.ml + test sur unification avec
 let-in.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16344 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/evars.v | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 4c77e4bcfd..ef2164a942 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -392,3 +392,10 @@ Definition tri_iffT : tri iffT iffT iffT :=
     (fun X0 X1 X2 E01 E02 =>
      (mkIff _ _ (fun x1 => iffLR _ _ E02 (iffRL _ _ E01 x1))
      (fun x2 => iffLR _ _ E01 (iffRL _ _ E02 x2))))).
+
+(* Check that local defs names are preserved if possible during unification *)
+
+Goal forall x (x':=x) (f:forall y, y=y:>nat -> Prop), f _ (eq_refl x').
+intros.
+unfold x' at 2. (* A way to check that there are indeed 2 occurrences of x' *)
+Abort.
-- 
cgit v1.2.3