diff options
| author | Hugo Herbelin | 2015-01-19 17:42:17 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-01-19 17:42:28 +0100 |
| commit | 9cc95f5a34b9050fe5a869f0fb96da562b45353d (patch) | |
| tree | 213be33b3bf8e7b56add18796c4d93862f468a4a | |
| parent | 9e6b28c04ad98369a012faf3bd4d630cf123a473 (diff) | |
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.
| -rw-r--r-- | pretyping/evarconv.ml | 3 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3929.v | 12 |
2 files changed, 13 insertions, 2 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index a95af2532f..616ceeabdc 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -555,8 +555,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | 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 t1 t2); - (fun i -> evar_conv_x ts env i CONV b1 b2); + [(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 diff --git a/test-suite/bugs/closed/3929.v b/test-suite/bugs/closed/3929.v new file mode 100644 index 0000000000..4031dcc45e --- /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. + |