Univ.constraints made fully abstract instead of being a Set of abstract stuff

 No need to tell the world about the fact that constraints are
 implemented via caml's Set. Other modules just need to know about
 the empty and union functions (and addition functions "enforce_geq"
 and "enforce_eq" that were already there).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13725 85f007b7-540e-0410-9357-904b9bb8a0f7

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