From 0767b8eace843ee45f2f3fc2b80a13ce6ed336c7 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 16 Jun 2016 11:11:01 +0200
Subject: Refine 9cc95f5, unification of Let-In's, bug #3929

We unify types of let-ins in FO heuristic before their bodies, using
cumulativity in either direction. This maintains the invariant that we
are comparing terms in related types throughout unification.
Also adapt test-suite file for bug #3929.
---
 pretyping/evarconv.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'pretyping/evarconv.ml')

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index e5fc5a188d..912fd198b6 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -590,9 +590,12 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     | MaybeFlexible v1, MaybeFlexible v2 -> begin
         match kind_of_term term1, kind_of_term term2 with
         | LetIn (na1,b1,t1,c'1), LetIn (na2,b2,t2,c'2) ->
-        let f1 i =
+        let f1 i = (* FO *)
           ise_and i
-	    [(fun i -> evar_conv_x ts env i CONV b1 b2);
+            [(fun i -> ise_try i
+               [(fun i -> evar_conv_x ts env i CUMUL t1 t2);
+                (fun i -> evar_conv_x ts env i CUMUL t2 t1)]);
+             (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