diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-11 10:40:18 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-11 13:30:33 +0200 |
| commit | 6e2b4a66b9f176555eb541cbee762d3cf3fc183c (patch) | |
| tree | 94e97abd5ddd41aed116eaa4791cf4de4d77d86b /pretyping/unification.ml | |
| parent | 0b6bb113559381f05a101f4b288c359539f48a1a (diff) | |
Fix bug #3505.
When w_unifying primitive projection applications, force
the unification of types of the projected records to recover instances
for the parameters (evarconv does this automatically by unifying evar
instances with their expected type).
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 9737b9feb..d89cde1ae 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -676,14 +676,12 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag | Proj (p1,c1), Proj (p2,c2) -> if eq_constant p1 p2 then try - let c1, c2, substn = - if isCast c1 && isCast c2 then - let (c1,_,tc1) = destCast c1 in - let (c2,_,tc2) = destCast c2 in - c1, c2, unirec_rec curenvnb CONV true false substn tc1 tc2 - else c1, c2, substn - in - unirec_rec curenvnb CONV true wt substn c1 c2 + let substn = unirec_rec curenvnb CONV true wt substn c1 c2 in + try (* Force unification of the types to fill in parameters *) + let ty1 = get_type_of curenv ~lax:true sigma c1 in + let ty2 = get_type_of curenv ~lax:true sigma c2 in + unirec_rec curenvnb CONV true false substn ty1 ty2 + with RetypeError _ -> substn with ex when precatchable_exception ex -> unify_not_same_head curenvnb pb b wt substn cM cN else |