From a4d454beaafd030a5564a395d380748cf90e1b75 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 1 Sep 2014 15:59:34 +0200
Subject: In evarconv, do first-order unification of LetIn's properly, ensuring
 we compare bodies of convertible types! Bug found by B. Ziliani.

---
 pretyping/evarconv.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 627a954f9d..edd1080713 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -483,10 +483,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 
     | MaybeFlexible (v1,sk1'), MaybeFlexible (v2,sk2') -> begin
         match kind_of_term term1, kind_of_term term2 with
-        | LetIn (na,b1,t1,c'1), LetIn (_,b2,_,c'2) ->
+        | LetIn (na,b1,t1,c'1), LetIn (_,b2,t2,c'2) ->
         let f1 i =
           ise_and i
-	    [(fun i -> evar_conv_x ts env i CONV b1 b2);
+	    [(fun i -> evar_conv_x ts env i CONV t1 t2);
+	     (fun i -> evar_conv_x ts env i CONV b1 b2);
 	     (fun i ->
 	       let b = nf_evar i b1 in
 	       let t = nf_evar i t1 in
-- 
cgit v1.2.3