aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/environ.ml2
-rw-r--r--checker/indtypes.ml2
-rw-r--r--checker/mod_checking.ml8
-rw-r--r--checker/typeops.ml2
-rw-r--r--kernel/environ.ml2
-rw-r--r--kernel/indtypes.ml6
-rw-r--r--kernel/inductive.ml6
-rw-r--r--kernel/mod_typing.ml48
-rw-r--r--kernel/reduction.ml12
-rw-r--r--kernel/safe_typing.ml24
-rw-r--r--kernel/subtyping.ml6
-rw-r--r--kernel/term_typing.ml4
-rw-r--r--kernel/typeops.ml22
-rw-r--r--kernel/univ.ml4
-rw-r--r--kernel/univ.mli5
-rw-r--r--kernel/vconv.ml4
-rw-r--r--pretyping/inductiveops.ml2
17 files changed, 81 insertions, 78 deletions
diff --git a/checker/environ.ml b/checker/environ.ml
index 8c23a7e46..d960e2a7c 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -98,7 +98,7 @@ let named_type id env =
(* Universe constraints *)
let add_constraints c env =
- if c == Constraint.empty then
+ if c == empty_constraint then
env
else
let s = env.env_stratification in
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 5de03b16d..1e773df65 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -176,7 +176,7 @@ let check_predicativity env s small level =
Type u, _ ->
let u' = fresh_local_univ () in
let cst =
- merge_constraints (enforce_geq u' u Constraint.empty)
+ merge_constraints (enforce_geq u' u empty_constraint)
(universes env) in
if not (check_geq cst u' level) then
failwith "impredicative Type inductive type"
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 78408c68c..30149331e 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -21,8 +21,8 @@ let refresh_arity ar =
Sort (Type u) when not (Univ.is_univ_variable u) ->
let u' = Univ.fresh_local_univ() in
mkArity (ctxt,Type u'),
- Univ.enforce_geq u' u Univ.Constraint.empty
- | _ -> ar, Univ.Constraint.empty
+ Univ.enforce_geq u' u Univ.empty_constraint
+ | _ -> ar, Univ.empty_constraint
let check_constant_declaration env kn cb =
Flags.if_verbose msgnl (str " checking cst: " ++ prcon kn);
@@ -247,12 +247,12 @@ and check_module env mp mb =
{typ_mp=mp;
typ_expr=sign;
typ_expr_alg=None;
- typ_constraints=Univ.Constraint.empty;
+ typ_constraints=Univ.empty_constraint;
typ_delta = mb.mod_delta;}
{typ_mp=mp;
typ_expr=mb.mod_type;
typ_expr_alg=None;
- typ_constraints=Univ.Constraint.empty;
+ typ_constraints=Univ.empty_constraint;
typ_delta = mb.mod_delta;};
and check_structure_field env mp lab res = function
diff --git a/checker/typeops.ml b/checker/typeops.ml
index c37f371f5..5226db534 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -255,7 +255,7 @@ let refresh_arity env ar =
match hd with
Sort (Type u) when not (is_univ_variable u) ->
let u' = fresh_local_univ() in
- let env' = add_constraints (enforce_geq u' u Constraint.empty) env in
+ let env' = add_constraints (enforce_geq u' u empty_constraint) env in
env', mkArity (ctxt,Type u')
| _ -> env, ar
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 33001ab74..34074b677 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -202,7 +202,7 @@ let set_universes g env =
{ env.env_stratification with env_universes = g } }
let add_constraints c env =
- if c == Constraint.empty then
+ if c == empty_constraint then
env
else
let s = env.env_stratification in
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 383bdc2ef..0798bf18a 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -160,7 +160,7 @@ let inductive_levels arities inds =
arity or type constructor; we do not to recompute universes constraints *)
let constraint_list_union =
- List.fold_left Constraint.union Constraint.empty
+ List.fold_left union_constraints empty_constraint
let infer_constructor_packet env_ar_par params lc =
(* type-check the constructors *)
@@ -197,7 +197,7 @@ let typecheck_inductive env mie =
full_arity is used as argument or subject to cast, an
upper universe will be generated *)
let full_arity = it_mkProd_or_LetIn arity.utj_val params in
- let cst = Constraint.union cst cst2 in
+ let cst = union_constraints cst cst2 in
let id = ind.mind_entry_typename in
let env_ar' =
push_rel (Name id, None, full_arity)
@@ -226,7 +226,7 @@ let typecheck_inductive env mie =
infer_constructor_packet env_ar_par params ind.mind_entry_lc in
let consnames = ind.mind_entry_consnames in
let ind' = (arity_data,consnames,info,lc',cstrs_univ) in
- (ind'::inds, Constraint.union cst cst'))
+ (ind'::inds, union_constraints cst cst'))
mie.mind_entry_inds
arity_list
([],cst) in
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 289968eb5..07195c493 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -294,7 +294,7 @@ let is_correct_arity env c pj ind specif params =
let univ =
try conv env a1 a1'
with NotConvertible -> raise (LocalArity None) in
- srec (push_rel (na1,None,a1) env) t ar' (Constraint.union u univ)
+ srec (push_rel (na1,None,a1) env) t ar' (union_constraints u univ)
| Prod (_,a1,a2), [] -> (* whnf of t was not needed here! *)
let ksort = match kind_of_term (whd_betadeltaiota env a2) with
| Sort s -> family_of_sort s
@@ -304,13 +304,13 @@ let is_correct_arity env c pj ind specif params =
try conv env a1 dep_ind
with NotConvertible -> raise (LocalArity None) in
check_allowed_sort ksort specif;
- Constraint.union u univ
+ union_constraints u univ
| _, (_,Some _,_ as d)::ar' ->
srec (push_rel d env) (lift 1 pt') ar' u
| _ ->
raise (LocalArity None)
in
- try srec env pj.uj_type (List.rev arsign) Constraint.empty
+ try srec env pj.uj_type (List.rev arsign) empty_constraint
with LocalArity kinds ->
error_elim_arity env ind (elim_sorts specif) c pj kinds
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index e14e7c900..5a3dade53 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -88,8 +88,8 @@ and check_with_aux_def env sign with_decl mp equiv =
let typ = Typeops.type_of_constant_type env' cb.const_type in
let cst2 = Reduction.conv_leq env' j.uj_type typ in
let cst =
- Constraint.union
- (Constraint.union cb.const_constraints cst1)
+ union_constraints
+ (union_constraints cb.const_constraints cst1)
cst2 in
let body = Some (Declarations.from_val j.uj_val) in
let cb' = {cb with
@@ -100,7 +100,7 @@ and check_with_aux_def env sign with_decl mp equiv =
SEBstruct(before@((l,SFBconst(cb'))::after)),cb',cst
| Some b ->
let cst1 = Reduction.conv env' c (Declarations.force b) in
- let cst = Constraint.union cb.const_constraints cst1 in
+ let cst = union_constraints cb.const_constraints cst1 in
let body = Some (Declarations.from_val c) in
let cb' = {cb with
const_body = body;
@@ -165,7 +165,7 @@ and check_with_aux_mod env sign with_decl mp equiv =
match old.mod_expr with
None ->
begin
- try Constraint.union
+ try union_constraints
(check_subtypes env' mtb_mp1
(module_type_of_module env' None old))
old.mod_constraints
@@ -212,7 +212,7 @@ and check_with_aux_mod env sign with_decl mp equiv =
let mpnew = rebuild_mp mp' (List.map label_of_id idl) in
check_modpath_equiv env' mpnew mp;
SEBstruct(before@(l,spec)::after)
- ,equiv,Constraint.empty
+ ,equiv,empty_constraint
| _ ->
error_a_generative_module_expected l
end
@@ -240,14 +240,14 @@ and translate_module env mp inl me =
let sign,alg1,resolver,cst2 =
match me.mod_entry_type with
| None ->
- sign,None,resolver,Constraint.empty
+ sign,None,resolver,empty_constraint
| Some mte ->
let mtb = translate_module_type env mp inl mte in
let cst = check_subtypes env
{typ_mp = mp;
typ_expr = sign;
typ_expr_alg = None;
- typ_constraints = Constraint.empty;
+ typ_constraints = empty_constraint;
typ_delta = resolver;}
mtb
in
@@ -257,7 +257,7 @@ and translate_module env mp inl me =
mod_type = sign;
mod_expr = Some alg_implem;
mod_type_alg = alg1;
- mod_constraints = Univ.Constraint.union cst1 cst2;
+ mod_constraints = Univ.union_constraints cst1 cst2;
mod_delta = resolver;
mod_retroknowledge = []}
(* spiwack: not so sure about that. It may
@@ -270,7 +270,7 @@ and translate_struct_module_entry env mp inl mse = match mse with
| MSEident mp1 ->
let mb = lookup_module mp1 env in
let mb' = strengthen_and_subst_mb mb mp env false in
- mb'.mod_type, SEBident mp1, mb'.mod_delta,Univ.Constraint.empty
+ mb'.mod_type, SEBident mp1, mb'.mod_delta,Univ.empty_constraint
| MSEfunctor (arg_id, arg_e, body_expr) ->
let mtb = translate_module_type env (MPbound arg_id) inl arg_e in
let env' = add_module (module_body_of_type (MPbound arg_id) mtb)
@@ -278,7 +278,7 @@ and translate_struct_module_entry env mp inl mse = match mse with
let sign,alg,resolver,cst =
translate_struct_module_entry env' mp inl body_expr in
SEBfunctor (arg_id, mtb, sign),SEBfunctor (arg_id, mtb, alg),resolver,
- Univ.Constraint.union cst mtb.typ_constraints
+ Univ.union_constraints cst mtb.typ_constraints
| MSEapply (fexpr,mexpr) ->
let sign,alg,resolver,cst1 =
translate_struct_module_entry env mp inl fexpr
@@ -300,24 +300,24 @@ and translate_struct_module_entry env mp inl mse = match mse with
let subst = map_mbid farg_id mp1 mp_delta in
(subst_struct_expr subst fbody_b),SEBapply(alg,SEBident mp1,cst),
(subst_codom_delta_resolver subst resolver),
- Univ.Constraint.union cst1 cst
+ Univ.union_constraints cst1 cst
| MSEwith(mte, with_decl) ->
let sign,alg,resolve,cst1 = translate_struct_module_entry env mp inl mte in
let sign,alg,resolve,cst2 = check_with env sign with_decl (Some alg) mp resolve in
- sign,Option.get alg,resolve,Univ.Constraint.union cst1 cst2
+ sign,Option.get alg,resolve,Univ.union_constraints cst1 cst2
and translate_struct_type_entry env inl mse = match mse with
| MSEident mp1 ->
let mtb = lookup_modtype mp1 env in
mtb.typ_expr,
- Some (SEBident mp1),mtb.typ_delta,mp1,Univ.Constraint.empty
+ Some (SEBident mp1),mtb.typ_delta,mp1,Univ.empty_constraint
| MSEfunctor (arg_id, arg_e, body_expr) ->
let mtb = translate_module_type env (MPbound arg_id) inl arg_e in
let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in
let sign,alg,resolve,mp_from,cst =
translate_struct_type_entry env' inl body_expr in
SEBfunctor (arg_id, mtb, sign),None,resolve,mp_from,
- Univ.Constraint.union cst mtb.typ_constraints
+ Univ.union_constraints cst mtb.typ_constraints
| MSEapply (fexpr,mexpr) ->
let sign,alg,resolve,mp_from,cst1 =
translate_struct_type_entry env inl fexpr
@@ -338,12 +338,12 @@ and translate_struct_type_entry env inl mse = match mse with
in
let subst = map_mbid farg_id mp1 mp_delta in
(subst_struct_expr subst fbody_b),None,
- (subst_codom_delta_resolver subst resolve),mp_from,Univ.Constraint.union cst1 cst2
+ (subst_codom_delta_resolver subst resolve),mp_from,Univ.union_constraints cst1 cst2
| MSEwith(mte, with_decl) ->
let sign,alg,resolve,mp_from,cst = translate_struct_type_entry env inl mte in
let sign,alg,resolve,cst1 =
check_with env sign with_decl alg mp_from resolve in
- sign,alg,resolve,mp_from,Univ.Constraint.union cst cst1
+ sign,alg,resolve,mp_from,Univ.union_constraints cst cst1
and translate_module_type env mp inl mte =
let sign,alg,resolve,mp_from,cst = translate_struct_type_entry env inl mte in
@@ -360,7 +360,7 @@ let rec translate_struct_include_module_entry env mp inl mse = match mse with
let mb = lookup_module mp1 env in
let mb' = strengthen_and_subst_mb mb mp env true in
let mb_typ = clean_bounded_mod_expr mb'.mod_type in
- mb_typ, mb'.mod_delta,Univ.Constraint.empty
+ mb_typ, mb'.mod_delta,Univ.empty_constraint
| MSEapply (fexpr,mexpr) ->
let sign,resolver,cst1 =
translate_struct_include_module_entry env mp inl fexpr in
@@ -381,7 +381,7 @@ let rec translate_struct_include_module_entry env mp inl mse = match mse with
let subst = map_mbid farg_id mp1 mp_delta in
(subst_struct_expr subst fbody_b),
(subst_codom_delta_resolver subst resolver),
- Univ.Constraint.union cst1 cst
+ Univ.union_constraints cst1 cst
| _ -> error ("You cannot Include a high-order structure.")
@@ -445,11 +445,11 @@ let rec struct_expr_constraints cst = function
| SEBapply (meb1,meb2,cst1) ->
struct_expr_constraints
- (struct_expr_constraints (Univ.Constraint.union cst1 cst) meb1)
+ (struct_expr_constraints (Univ.union_constraints cst1 cst) meb1)
meb2
| SEBwith(meb,With_definition_body(_,cb))->
struct_expr_constraints
- (Univ.Constraint.union cb.const_constraints cst) meb
+ (Univ.union_constraints cb.const_constraints cst) meb
| SEBwith(meb,With_module_body(_,_))->
struct_expr_constraints cst meb
@@ -465,11 +465,11 @@ and module_constraints cst mb =
| Some meb -> struct_expr_constraints cst meb in
let cst =
struct_expr_constraints cst mb.mod_type in
- Univ.Constraint.union mb.mod_constraints cst
+ Univ.union_constraints mb.mod_constraints cst
and modtype_constraints cst mtb =
- struct_expr_constraints (Univ.Constraint.union mtb.typ_constraints cst) mtb.typ_expr
+ struct_expr_constraints (Univ.union_constraints mtb.typ_constraints cst) mtb.typ_expr
-let struct_expr_constraints = struct_expr_constraints Univ.Constraint.empty
-let module_constraints = module_constraints Univ.Constraint.empty
+let struct_expr_constraints = struct_expr_constraints Univ.empty_constraint
+let module_constraints = module_constraints Univ.empty_constraint
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index cbcbd151e..c865c92bf 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -197,9 +197,9 @@ let sort_cmp pb s0 s1 cuniv =
| (_, _) -> raise NotConvertible
-let conv_sort env s0 s1 = sort_cmp CONV s0 s1 Constraint.empty
+let conv_sort env s0 s1 = sort_cmp CONV s0 s1 empty_constraint
-let conv_sort_leq env s0 s1 = sort_cmp CUMUL s0 s1 Constraint.empty
+let conv_sort_leq env s0 s1 = sort_cmp CUMUL s0 s1 empty_constraint
let rec no_arg_available = function
| [] -> true
@@ -426,10 +426,10 @@ and convert_vect infos lft1 lft2 v1 v2 cuniv =
let clos_fconv trans cv_pb evars env t1 t2 =
let infos = trans, create_clos_infos ~evars betaiotazeta env in
- ccnv cv_pb infos ELID ELID (inject t1) (inject t2) Constraint.empty
+ ccnv cv_pb infos ELID ELID (inject t1) (inject t2) empty_constraint
let trans_fconv reds cv_pb evars env t1 t2 =
- if eq_constr t1 t2 then Constraint.empty
+ if eq_constr t1 t2 then empty_constraint
else clos_fconv reds cv_pb evars env t1 t2
let trans_conv_cmp conv reds = trans_fconv reds conv (fun _->None)
@@ -448,8 +448,8 @@ let conv_leq_vecti ?(evars=fun _->None) env v1 v2 =
let c' =
try conv_leq ~evars env t1 t2
with NotConvertible -> raise (NotConvertibleVect i) in
- Constraint.union c c')
- Constraint.empty
+ union_constraints c c')
+ empty_constraint
v1
v2
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 517a9c809..2bed2bb48 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=[];
}
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 8e74ff725..93844ce5b 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -69,7 +69,7 @@ let make_label_map mp list =
let check_conv_error error cst f env a1 a2 =
try
- Constraint.union cst (f env a1 a2)
+ union_constraints cst (f env a1 a2)
with
NotConvertible -> error ()
@@ -369,7 +369,7 @@ and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv =
if equiv then
let subst2 =
add_mp mtb2.typ_mp mtb1.typ_mp mtb1.typ_delta subst2 in
- Univ.Constraint.union
+ Univ.union_constraints
(check_signatures cst env
mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2
mtb1.typ_delta mtb2.typ_delta)
@@ -413,7 +413,7 @@ and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv =
let check_subtypes env sup super =
let env = add_module
(module_body_of_type sup.typ_mp sup) env in
- check_modtypes Constraint.empty env
+ check_modtypes empty_constraint env
(strengthen env sup sup.typ_mp) super empty_subst
(map_mp super.typ_mp sup.typ_mp sup.typ_delta) false
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index ab3e78fbc..f765dd77e 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -33,7 +33,7 @@ let constrain_type env j cst1 = function
let (tj,cst2) = infer_type env t in
let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
assert (t = tj.utj_val);
- NonPolymorphicType t, Constraint.union (Constraint.union cst1 cst2) cst3
+ NonPolymorphicType t, union_constraints (union_constraints cst1 cst2) cst3
let local_constrain_type env j cst1 = function
| None ->
@@ -42,7 +42,7 @@ let local_constrain_type env j cst1 = function
let (tj,cst2) = infer_type env t in
let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
assert (t = tj.utj_val);
- t, Constraint.union (Constraint.union cst1 cst2) cst3
+ t, union_constraints (union_constraints cst1 cst2) cst3
let translate_local_def env (b,topt) =
let (j,cst) = infer env b in
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 3d2461237..3568118cf 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -26,8 +26,8 @@ let conv_leq_vecti env v1 v2 =
let c' =
try default_conv CUMUL env t1 t2
with NotConvertible -> raise (NotConvertibleVect i) in
- Constraint.union c c')
- Constraint.empty
+ union_constraints c c')
+ empty_constraint
v1
v2
@@ -202,7 +202,7 @@ let judge_of_apply env funj argjv =
| Prod (_,c1,c2) ->
(try
let c = conv_leq env hj.uj_type c1 in
- let cst' = Constraint.union cst c in
+ let cst' = union_constraints cst c in
apply_rec (n+1) (subst1 hj.uj_val c2) cst' restjl
with NotConvertible ->
error_cant_apply_bad_type env
@@ -214,7 +214,7 @@ let judge_of_apply env funj argjv =
in
apply_rec 1
funj.uj_type
- Constraint.empty
+ empty_constraint
(Array.to_list argjv)
(* Type of product *)
@@ -332,7 +332,7 @@ let judge_of_case env ci pj cj lfj =
({ uj_val = mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val,
Array.map j_val lfj);
uj_type = rslty },
- Constraint.union univ univ')
+ union_constraints univ univ')
(* Fixpoints. *)
@@ -354,7 +354,7 @@ let type_fixpoint env lna lar vdefj =
graph and in the universes of the environment. This is to ensure
that the infered local graph is satisfiable. *)
let univ_combinator (cst,univ) (j,c') =
- (j,(Constraint.union cst c', merge_constraints c' univ))
+ (j,(union_constraints cst c', merge_constraints c' univ))
(* The typing machine. *)
(* ATTENTION : faudra faire le typage du contexte des Const,
@@ -474,18 +474,18 @@ and execute_array env = array_fold_map' (execute env)
(* Derived functions *)
let infer env constr =
let (j,(cst,_)) =
- execute env constr (Constraint.empty, universes env) in
+ execute env constr (empty_constraint, universes env) in
assert (j.uj_val = constr);
({ j with uj_val = constr }, cst)
let infer_type env constr =
let (j,(cst,_)) =
- execute_type env constr (Constraint.empty, universes env) in
+ execute_type env constr (empty_constraint, universes env) in
(j, cst)
let infer_v env cv =
let (jv,(cst,_)) =
- execute_array env cv (Constraint.empty, universes env) in
+ execute_array env cv (empty_constraint, universes env) in
(jv, cst)
(* Typing of several terms. *)
@@ -503,8 +503,8 @@ let infer_local_decls env decls =
| (id, d) :: l ->
let env, l, cst1 = inferec env l in
let d, cst2 = infer_local_decl env id d in
- push_rel d env, add_rel_decl d l, Constraint.union cst1 cst2
- | [] -> env, empty_rel_context, Constraint.empty in
+ push_rel d env, add_rel_decl d l, union_constraints cst1 cst2
+ | [] -> env, empty_rel_context, empty_constraint in
inferec env decls
(* Exported typing functions *)
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 6fa8d5bc5..8db4484b6 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -447,7 +447,6 @@ let enforce_constraint cst g =
| (u,Le,v) -> enforce_univ_leq u v g
| (u,Eq,v) -> enforce_univ_eq u v g
-
module Constraint = Set.Make(
struct
type t = univ_constraint
@@ -456,6 +455,9 @@ module Constraint = Set.Make(
type constraints = Constraint.t
+let empty_constraint = Constraint.empty
+let union_constraints = Constraint.union
+
type constraint_function =
universe -> universe -> constraints -> constraints
diff --git a/kernel/univ.mli b/kernel/univ.mli
index e9f25fe85..268321ece 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -42,9 +42,10 @@ val initial_universes : universes
(** {6 Constraints. } *)
-module Constraint : Set.S
+type constraints
-type constraints = Constraint.t
+val empty_constraint : constraints
+val union_constraints : constraints -> constraints -> constraints
type constraint_function = universe -> universe -> constraints -> constraints
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index a35d1d88e..96445f696 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -219,12 +219,12 @@ and conv_eq_vect vt1 vt2 cu =
let vconv pb env t1 t2 =
let cu =
- try conv_eq pb t1 t2 Constraint.empty
+ try conv_eq pb t1 t2 empty_constraint
with NotConvertible ->
infos := create_clos_infos betaiotazeta env;
let v1 = val_of_constr env t1 in
let v2 = val_of_constr env t2 in
- let cu = conv_val pb (nb_rel env) v1 v2 Constraint.empty in
+ let cu = conv_val pb (nb_rel env) v1 v2 empty_constraint in
cu
in cu
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 5bd8b44f9..15fd226f1 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -402,7 +402,7 @@ let is_constrained is u =
let _ =
merge_constraints
(enforce_geq u (super u')
- (enforce_geq u' is Constraint.empty))
+ (enforce_geq u' is empty_constraint))
initial_universes in
false
with UniverseInconsistency _ -> true
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-04 20:16:35 +0000