diff options
| author | herbelin | 2007-05-24 12:16:09 +0000 |
|---|---|---|
| committer | herbelin | 2007-05-24 12:16:09 +0000 |
| commit | a11acc8e5008d988451ffec989be6be07bdc43b9 (patch) | |
| tree | a5095420b4046d36a029d07e85cd334c30291021 /pretyping | |
| parent | 9b4967f77498f83c0ad37598a0338947c4f276ab (diff) | |
Unification suite: petits affinements pour préserver la compatibilité
(en particulier, la décision de quelle instance garder quand une méta
a plusieurs solutions importe; comment trouver une critère objectif ?
la compatibilité demande à donner préférence aux instances trouvées
par with-bindings).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9855 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/clenv.ml | 3 | ||||
| -rw-r--r-- | pretyping/unification.ml | 6 |
2 files changed, 5 insertions, 4 deletions
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index a08c626256..edf9056419 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -409,7 +409,8 @@ let clenv_unify_similar_types clenv c t u = let clenv_assign_binding clenv k (sigma,c) = let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in let clenv' = { clenv with evd = evar_merge clenv.evd sigma} in - let c_typ = clenv_hnf_constr clenv' (clenv_get_type_of clenv' c) in + let c_typ = nf_betaiota (clenv_get_type_of clenv' c) in + let c_typ = clenv_hnf_constr clenv' c_typ in let status,clenv'',c = clenv_unify_similar_types clenv' c c_typ k_typ in (* let evd,c' = w_coerce (cl_env clenv') c c_typ k_typ clenv'.evd in*) { clenv'' with evd = meta_assign k (c,status) clenv''.evd } diff --git a/pretyping/unification.ml b/pretyping/unification.ml index bd6fb5ad88..372188e8a0 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -183,9 +183,9 @@ let unify_0_with_initial_metas metas env sigma cv_pb mod_delta m n = (if mod_delta then is_fconv (conv_pb_of cv_pb) env sigma m n else eq_constr m n) then - (metas,[]) + ([],[]) else - let (mc,ec) = unirec_rec env cv_pb (metas,[]) m n in + let (mc,ec) = unirec_rec env cv_pb ([],[]) m n in ((*sort_eqns*) mc, (*sort_eqns*) ec) let unify_0 = unify_0_with_initial_metas [] @@ -442,7 +442,7 @@ let w_unify_core_0 env with_types cv_pb mod_delta m n evd = let (mc1,evd') = retract_coercible_metas evd in let (mc2,ec) = unify_0_with_initial_metas mc1 env (evars_of evd') cv_pb mod_delta m n in - w_merge env with_types mod_delta mc2 ec evd' + w_merge env with_types mod_delta (mc1@mc2) ec evd' let w_unify_0 env = w_unify_core_0 env false let w_typed_unify env = w_unify_core_0 env true |