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

1 files changed, 12 insertions, 12 deletions

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=[];
   }