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

1 files changed, 7 insertions, 0 deletions

diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 4c77e4bcf..ef2164a94 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.