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.

1 files changed, 56 insertions, 1 deletions

diff --git a/test-suite/bugs/closed/3929.v b/test-suite/bugs/closed/3929.v
index 4031dcc45..955581ef2 100644
--- a/test-suite/bugs/closed/3929.v
+++ b/test-suite/bugs/closed/3929.v
@@ -1,5 +1,36 @@
+Universes i j.
+Set Printing Universes.
+Set Printing All.
+Polymorphic Definition lt@{x y} : Type@{y} := Type@{x}.
 Goal True.
-evar (T:Type).
+evar (T:Type@{i}).
+set (Z := nat : Type@{j}). simpl in Z.
+let Tv:=eval cbv [T] in T in
+pose (x:=Tv).
+revert x.
+refine (_ : let x:=Z in True).
+(** This enforces i <= j *)
+Fail pose (lt@{i j}).
+let Zv:=eval cbv [Z] in Z in
+let Tv:=eval cbv [T] in T in
+constr_eq Zv Tv.
+exact I. 
+Defined.
+
+Goal True.
+evar (T:nat).
+pose (Z:=0).
+let Tv:=eval cbv [T] in T in
+pose (x:=Tv).
+revert x.
+refine (_ : let x:=Z in True).
+let Zv:=eval cbv [Z] in Z in
+let Tv:=eval cbv [T] in T in
+constr_eq Zv Tv.
+Abort.
+
+Goal True.
+evar (T:Set).
 pose (Z:=nat).
 let Tv:=eval cbv [T] in T in
 pose (x:=Tv).
@@ -10,3 +41,27 @@ let Tv:=eval cbv [T] in T in
 constr_eq Zv Tv.
 Abort.
 
+Goal forall (A:Type)(a:A), True.
+intros A a.
+evar (T:A).
+pose (Z:=a).
+let Tv:=eval cbv delta [T] in T in
+pose (x:=Tv).
+revert x.
+refine (_ : let x:=Z in True).
+let Zv:=eval cbv [Z] in Z in
+let Tv:=eval cbv [T] in T in
+constr_eq Zv Tv.
+Abort.
+
+Goal True.
+evar (T:Type).
+pose (Z:=nat).
+let Tv:=eval cbv [T] in T in
+pose (x:=Tv).
+revert x.
+refine (_ : let x:=Z in True).
+let Zv:=eval cbv [Z] in Z in
+let Tv:=eval cbv [T] in T in
+constr_eq Zv Tv.
+Abort.