Making unification of LetIn's expressions more consistent (see #3920).

Unifying two let-in's expresions syntactically is a heuristic
(compared to performing the zeta-reduction). This heuristic was
requiring unification of types which is too strong for the heuristic
to work uniformly since the types might only be related modulo
subtyping.

The patch is to remove the unification of types, which allows then to
have the heuristic work uniformly on the bodies. On the other side, I
hope it does not loose (still heuristical) unifications compared to
before (presumably, since instantiating the evars in the body will
induce constraints for solving potential evars in the types of the
let-in bodies, but this would need a proof). Anyway, it is not about
correction, it is about a heuristic, which maybe done too early
actually.

1 files changed, 12 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3929.v b/test-suite/bugs/closed/3929.v
new file mode 100644
index 000000000..4031dcc45
--- /dev/null
+++ b/test-suite/bugs/closed/3929.v
@@ -0,0 +1,12 @@
+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.
+