diff options
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 517a9c8099..2bed2bb484 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -135,7 +135,7 @@ let rec empty_environment = resolver_of_param = empty_delta_resolver}; labset = Labset.empty; revstruct = []; - univ = Univ.Constraint.empty; + univ = Univ.empty_constraint; engagement = None; imports = []; loads = []; @@ -153,7 +153,7 @@ let env_of_senv = env_of_safe_env let add_constraints cst senv = {senv with env = Environ.add_constraints cst senv.env; - univ = Univ.Constraint.union cst senv.univ } + univ = Univ.union_constraints cst senv.univ } (*spiwack: functions for safe retroknowledge *) @@ -377,7 +377,7 @@ let start_module l senv = modinfo = modinfo; labset = Labset.empty; revstruct = []; - univ = Univ.Constraint.empty; + univ = Univ.empty_constraint; engagement = None; imports = senv.imports; loads = []; @@ -411,13 +411,13 @@ let end_module l restype senv = let mexpr,mod_typ,mod_typ_alg,resolver,cst = match restype with | None -> let mexpr = functorize_struct auto_tb in - mexpr,mexpr,None,modinfo.resolver,Constraint.empty + mexpr,mexpr,None,modinfo.resolver,empty_constraint | Some mtb -> let auto_mtb = { typ_mp = senv.modinfo.modpath; typ_expr = auto_tb; typ_expr_alg = None; - typ_constraints = Constraint.empty; + typ_constraints = empty_constraint; typ_delta = empty_delta_resolver} in let cst = check_subtypes senv.env auto_mtb mtb in @@ -427,7 +427,7 @@ let end_module l restype senv = Option.map functorize_struct mtb.typ_expr_alg in mexpr,mod_typ,typ_alg,mtb.typ_delta,cst in - let cst = Constraint.union cst senv.univ in + let cst = union_constraints cst senv.univ in let mb = { mod_mp = mp; mod_expr = Some mexpr; @@ -461,7 +461,7 @@ let end_module l restype senv = modinfo = modinfo; labset = Labset.add l oldsenv.labset; revstruct = (l,SFBmodule mb)::oldsenv.revstruct; - univ = Univ.Constraint.union senv'.univ oldsenv.univ; + univ = Univ.union_constraints senv'.univ oldsenv.univ; (* engagement is propagated to the upper level *) engagement = senv'.engagement; imports = senv'.imports; @@ -503,7 +503,7 @@ let end_module l restype senv = let resolver,sign,senv = compute_sign sign {typ_mp = mp_sup; typ_expr = SEBstruct (List.rev senv.revstruct); typ_expr_alg = None; - typ_constraints = Constraint.empty; + typ_constraints = empty_constraint; typ_delta = senv.modinfo.resolver} resolver senv in let str = match sign with | SEBstruct(str_l) -> str_l @@ -636,7 +636,7 @@ let start_modtype l senv = modinfo = modinfo; labset = Labset.empty; revstruct = []; - univ = Univ.Constraint.empty; + univ = Univ.empty_constraint; engagement = None; imports = senv.imports; loads = [] ; @@ -687,7 +687,7 @@ let end_modtype l senv = modinfo = oldsenv.modinfo; labset = Labset.add l oldsenv.labset; revstruct = (l,SFBmodtype mtb)::oldsenv.revstruct; - univ = Univ.Constraint.union senv.univ oldsenv.univ; + univ = Univ.union_constraints senv.univ oldsenv.univ; engagement = senv.engagement; imports = senv.imports; loads = senv.loads@oldsenv.loads; @@ -746,7 +746,7 @@ let start_library dir senv = modinfo = modinfo; labset = Labset.empty; revstruct = []; - univ = Univ.Constraint.empty; + univ = Univ.empty_constraint; engagement = None; imports = senv.imports; loads = []; @@ -757,7 +757,7 @@ let pack_module senv = mod_expr=None; mod_type= SEBstruct (List.rev senv.revstruct); mod_type_alg=None; - mod_constraints=Constraint.empty; + mod_constraints=empty_constraint; mod_delta=senv.modinfo.resolver; mod_retroknowledge=[]; } |