Removing 'open Univ' from checker.

7 files changed, 35 insertions, 42 deletions

diff --git a/checker/environ.ml b/checker/environ.ml
index d23740ca7a..a04e95cfc4 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -1,7 +1,6 @@
 open Errors
 open Util
 open Names
-open Univ
 open Cic
 open Term
 open Declarations
@@ -14,7 +13,7 @@ type globals = {
   env_modtypes : module_type_body MPmap.t}
 
 type stratification = {
-  env_universes : universes;
+  env_universes : Univ.universes;
   env_engagement : engagement option
 }
 
@@ -77,12 +76,12 @@ let push_rec_types (lna,typarray,_) env =
 
 (* Universe constraints *)
 let add_constraints c env =
-  if c == Constraint.empty then
+  if c == Univ.Constraint.empty then
     env
   else
     let s = env.env_stratification in
     { env with env_stratification =
-      { s with env_universes = merge_constraints c s.env_universes } }
+      { s with env_universes = Univ.merge_constraints c s.env_universes } }
 
 let check_constraints cst env =
   Univ.check_constraints cst env.env_stratification.env_universes
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index bfc20d7f8f..14710c10b7 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -9,7 +9,6 @@
 open Errors
 open Util
 open Names
-open Univ
 open Cic
 open Term
 open Inductive
@@ -183,7 +182,7 @@ let check_predicativity env s small level =
         (* let cst = *)
         (*   merge_constraints (enforce_leq u u' empty_constraint) *)
         (*     (universes env) in *)
-        if not (check_leq (universes env) level u) then
+        if not (Univ.check_leq (universes env) level u) then
           failwith "impredicative Type inductive type"
     | Prop Pos, Some ImpredicativeSet -> ()
     | Prop Pos, _ ->
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 29eca3d828..3aab2e9429 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -9,7 +9,6 @@
 open Errors
 open Util
 open Names
-open Univ
 open Cic
 open Term
 open Reduction
@@ -56,7 +55,7 @@ let inductive_params (mib,_) = mib.mind_nparams
 
 let make_inductive_subst mib u =
   if mib.mind_polymorphic then 
-    make_universe_subst u mib.mind_universes
+    Univ.make_universe_subst u mib.mind_universes
   else Univ.empty_level_subst
 
 let inductive_params_ctxt (mib,u) = 
@@ -65,18 +64,18 @@ let inductive_params_ctxt (mib,u) =
 
 let inductive_instance mib =
   if mib.mind_polymorphic then 
-    UContext.instance mib.mind_universes
-  else Instance.empty
+    Univ.UContext.instance mib.mind_universes
+  else Univ.Instance.empty
 
 let inductive_context mib =
   if mib.mind_polymorphic then 
     mib.mind_universes 
-  else UContext.empty
+  else Univ.UContext.empty
 
 let instantiate_inductive_constraints mib subst =
   if mib.mind_polymorphic then
-    instantiate_univ_context subst mib.mind_universes
-  else Constraint.empty
+    Univ.instantiate_univ_context subst mib.mind_universes
+  else Univ.Constraint.empty
 
 (************************************************************************)
 
@@ -150,13 +149,13 @@ Remark: Set (predicative) is encoded as Type(0)
 
 let sort_as_univ = function
 | Type u -> u
-| Prop Null -> type0m_univ
-| Prop Pos -> type0_univ
+| Prop Null -> Univ.type0m_univ
+| Prop Pos -> Univ.type0_univ
 
 let cons_subst u su subst =
   try
-    (u, sup su (List.assoc_f Universe.equal u subst)) ::
-      List.remove_assoc_f Universe.equal u subst
+    (u, Univ.sup su (List.assoc_f Univ.Universe.equal u subst)) ::
+      List.remove_assoc_f Univ.Universe.equal u subst
   with Not_found -> (u, su) :: subst
 
 let actualize_decl_level env lev t =
@@ -208,12 +207,12 @@ exception SingletonInductiveBecomesProp of Id.t
 let instantiate_universes env ctx ar argsorts =
   let args = Array.to_list argsorts in
   let ctx,subst = make_subst env (ctx,ar.template_param_levels,args) in
-  let level = subst_large_constraints subst ar.template_level in
+  let level = Univ.subst_large_constraints subst ar.template_level in
   let ty =
     (* Singleton type not containing types are interpretable in Prop *)
-    if is_type0m_univ level then Prop Null
+    if Univ.is_type0m_univ level then Prop Null
     (* Non singleton type not containing types are interpretable in Set *)
-    else if is_type0_univ level then Prop Pos
+    else if Univ.is_type0_univ level then Prop Pos
     (* This is a Type with constraints *)
     else Type level
   in
@@ -238,7 +237,7 @@ let type_of_inductive_subst ?(polyprop=true) env ((mib,mip),u) paramtyps =
       (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e.
          the situation where a non-Prop singleton inductive becomes Prop
          when applied to Prop params *)
-      if not polyprop && not (is_type0m_univ ar.template_level) && is_prop_sort s
+      if not polyprop && not (Univ.is_type0m_univ ar.template_level) && is_prop_sort s
       then raise (SingletonInductiveBecomesProp mip.mind_typename);
       mkArity (List.rev ctx,s), Univ.LMap.empty
 
@@ -255,7 +254,7 @@ let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps =
       (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e.
          the situation where a non-Prop singleton inductive becomes Prop
          when applied to Prop params *)
-      if not polyprop && not (is_type0m_univ ar.template_level) && is_prop_sort s
+      if not polyprop && not (Univ.is_type0m_univ ar.template_level) && is_prop_sort s
       then raise (SingletonInductiveBecomesProp mip.mind_typename);
       mkArity (List.rev ctx,s)
 
@@ -284,11 +283,11 @@ let type_of_inductive env mip =
 
 let cumulate_constructor_univ u = function
   | Prop Null -> u
-  | Prop Pos -> sup type0_univ u
-  | Type u' -> sup u u'
+  | Prop Pos -> Univ.sup Univ.type0_univ u
+  | Type u' -> Univ.sup u u'
 
 let max_inductive_sort =
-  Array.fold_left cumulate_constructor_univ type0m_univ
+  Array.fold_left cumulate_constructor_univ Univ.type0m_univ
 
 (************************************************************************)
 (* Type of a constructor *)
@@ -310,7 +309,7 @@ let type_of_constructor cstru mspec =
   fst (type_of_constructor_gen cstru mspec)
 
 let type_of_constructor_in_ctx cstr (mib,mip as mspec) =
-  let u = UContext.instance mib.mind_universes in
+  let u = Univ.UContext.instance mib.mind_universes in
   let c = type_of_constructor_gen (cstr, u) mspec in
     (fst c, mib.mind_universes)
 
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 49f0a26e72..289b9a7589 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -10,7 +10,6 @@ open Errors
 open Util
 open Cic
 open Term
-open Univ
 open Closure
 open Esubst
 open Environ
@@ -160,8 +159,8 @@ let sort_cmp univ pb s0 s1 =
     | (Type u1, Type u2) ->
         if not
 	  (match pb with
-            | CONV -> check_eq univ u1 u2
-	    | CUMUL -> check_leq univ u1 u2)
+            | CONV -> Univ.check_eq univ u1 u2
+	    | CUMUL -> Univ.check_leq univ u1 u2)
         then raise NotConvertible
     | (_, _) -> raise NotConvertible
 
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 6c66ca60b8..c4688e1904 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -10,7 +10,6 @@
 open Errors
 open Util
 open Names
-open Univ
 open Cic
 open Term
 open Declarations
@@ -99,8 +98,8 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
     check bool_equal (fun x -> x.mind_polymorphic);
     if mib1.mind_polymorphic then (
       check Univ.Instance.equal (fun x -> Univ.UContext.instance x.mind_universes);
-      UContext.instance mib1.mind_universes)
-    else Instance.empty
+      Univ.UContext.instance mib1.mind_universes)
+    else Univ.Instance.empty
   in
   let check_inductive_type env t1 t2 =
 
@@ -233,13 +232,13 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
       if isArity t2 then
         let (ctx2,s2) = destArity t2 in
         match s2 with
-        | Type v when not (is_univ_variable v) ->
+        | Type v when not (Univ.is_univ_variable v) ->
           (* The type in the interface is inferred and is made of algebraic
              universes *)
           begin try
             let (ctx1,s1) = dest_arity env t1 in
             match s1 with
-            | Type u when not (is_univ_variable u) ->
+            | Type u when not (Univ.is_univ_variable u) ->
               (* Both types are inferred, no need to recheck them. We
                  cheat and collapse the types to Prop *)
                 mkArity (ctx1,Prop Null), mkArity (ctx2,Prop Null)
diff --git a/checker/term.ml b/checker/term.ml
index 0f8aa804f6..3372f9b6c3 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -11,7 +11,6 @@
 open Errors
 open Util
 open Names
-open Univ
 open Esubst
 
 open Cic
@@ -349,7 +348,7 @@ let compare_sorts s1 s2 = match s1, s2 with
   | Pos, Null -> false
   | Null, Pos -> false
   end
-| Type u1, Type u2 -> Universe.equal u1 u2
+| Type u1, Type u2 -> Univ.Universe.equal u1 u2
 | Prop _, Type _ -> false
 | Type _, Prop _ -> false
 
diff --git a/checker/typeops.ml b/checker/typeops.ml
index a0640a55f3..77fc4af739 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -9,7 +9,6 @@
 open Errors
 open Util
 open Names
-open Univ
 open Cic
 open Term
 open Reduction
@@ -53,11 +52,11 @@ let assumption_of_judgment env j =
 
 (* Prop and Set *)
 
-let judge_of_prop = Sort (Type type1_univ)
+let judge_of_prop = Sort (Type Univ.type1_univ)
 
 (* Type of Type(i). *)
 
-let judge_of_type u = Sort (Type (super u))
+let judge_of_type u = Sort (Type (Univ.super u))
 
 (*s Type of a de Bruijn index. *)
 
@@ -134,13 +133,13 @@ let sort_of_product env domsort rangsort =
           rangsort
         else
           (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
-          Type (sup u1 type0_univ)
+          Type (Univ.sup u1 Univ.type0_univ)
     (* Product rule (Prop,Type_i,Type_i) *)
-    | (Prop Pos,  Type u2)  -> Type (sup type0_univ u2)
+    | (Prop Pos,  Type u2)  -> Type (Univ.sup Univ.type0_univ u2)
     (* Product rule (Prop,Type_i,Type_i) *)
     | (Prop Null, Type _)  -> rangsort
     (* Product rule (Type_i,Type_i,Type_i) *)
-    | (Type u1, Type u2) -> Type (sup u1 u2)
+    | (Type u1, Type u2) -> Type (Univ.sup u1 u2)
 
 (* Type of a type cast *)