diff options
| author | Matthieu Sozeau | 2014-09-15 12:10:57 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-15 12:16:52 +0200 |
| commit | 92682297f528c3570dc8449118d2f2cd2be7cc53 (patch) | |
| tree | b5e956779cea608343b5f1d5a07b9354a231a0c2 | |
| parent | d4edff8e7a070151da6536a9674b15993cc273b5 (diff) | |
Fix bug #3610, allowing betaiotadelta reduction while unifying types of
records in unification.ml.
| -rw-r--r-- | pretyping/unification.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index b07bf4f924..937d84972b 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -512,7 +512,7 @@ let eta_constructor_app env f l1 term = | _ -> assert false) | _ -> assert false -let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flags m n = +let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flags m n = let rec unirec_rec (curenv,nb as curenvnb) pb b wt ((sigma,metasubst,evarsubst) as substn) curm curn = let cM = Evarutil.whd_head_evar sigma curm and cN = Evarutil.whd_head_evar sigma curn in @@ -675,7 +675,10 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag 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 + unify_0_with_initial_metas substn true env cv_pb + { flags with modulo_delta = full_transparent_state; + modulo_betaiota = true } + ty1 ty2 with RetypeError _ -> substn with ex when precatchable_exception ex -> unify_not_same_head curenvnb pb b wt substn cM cN |