diff options
| author | herbelin | 2007-05-23 10:29:01 +0000 |
|---|---|---|
| committer | herbelin | 2007-05-23 10:29:01 +0000 |
| commit | b483e1732682bd1b8cec8d5d3a600c93d90f44ab (patch) | |
| tree | 73061a8da273c859530bbf90b61e8f9ad01ccb34 /pretyping/unification.ml | |
| parent | 500aaf4e5ab37550efc0e0493b0afa45eaf250d3 (diff) | |
Suite restructuration unification et division des problèmes
d'unification des types des with-bindings en deux: les problèmes
d'unification susceptibles d'introduire une coercion sont retardés
(comme dans le commit r9850) et ceux susceptibles de fournir d'autres
instances restent faits au plus tôt (comme avant le commit r9850).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9851 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index e296737f25..bd6fb5ad88 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -65,7 +65,7 @@ let prod_pb = function ConvUnderApp _ -> topconv | pb -> pb let opp_status = function | IsSuperType -> IsSubType | IsSubType -> IsSuperType - | ConvUpToEta _ | Coercible _ as x -> x + | ConvUpToEta _ | Coercible _ | Processed as x -> x let extract_instance_status = function | Cumul -> (IsSubType,IsSuperType) @@ -231,13 +231,13 @@ let merge_instances env sigma mod_delta st1 st2 c1 c2 = | (ConvUpToEta n1, ConvUpToEta n2) -> let side = left (* arbitrary choice, but agrees with compatibility *) in unify_with_eta side mod_delta env sigma n1 n2 c1 c2 - | ((IsSubType | ConvUpToEta _ | Coercible _ as oppst1), - (IsSubType | ConvUpToEta _ | Coercible _)) -> + | ((IsSubType | ConvUpToEta _ | Coercible _ | Processed as oppst1), + (IsSubType | ConvUpToEta _ | Coercible _ | Processed)) -> let res = unify_0 env sigma Cumul mod_delta c2 c1 in if oppst1=st2 then (* arbitrary choice *) (left, st1, res) else (st2=IsSubType, ConvUpToEta 0, res) - | ((IsSuperType | ConvUpToEta _ | Coercible _ as oppst1), - (IsSuperType | ConvUpToEta _ | Coercible _)) -> + | ((IsSuperType | ConvUpToEta _ | Coercible _ | Processed as oppst1), + (IsSuperType | ConvUpToEta _ | Coercible _ | Processed)) -> let res = unify_0 env sigma Cumul mod_delta c1 c2 in if oppst1=st2 then (* arbitrary choice *) (left, st1, res) else (st2=IsSuperType, ConvUpToEta 0, res) @@ -379,7 +379,7 @@ let w_merge env with_types mod_delta metas evars evd = else begin let evd,n = - if with_types (* or occur_meta mvty *) then + if with_types & status <> Processed then let sigma = evars_of evd in let metas = metas_of evd in let mvty = Typing.meta_type evd mv in @@ -439,7 +439,7 @@ let w_merge env with_types mod_delta metas evars evd = types of metavars are unifiable with the types of their instances *) let w_unify_core_0 env with_types cv_pb mod_delta m n evd = - let (mc1,evd') = retract_defined_metas evd in + 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' |