Make Sorts.t private

10 files changed, 23 insertions, 22 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 718584b3d4..af14baaca6 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -562,10 +562,10 @@ let rec compile_lam env cenv lam sz cont =
       compile_fv_elem cenv (FVuniv_var idx) sz cont
     in
     if List.is_empty s then
-      compile_structured_constant cenv (Const_sort (Sorts.Type u)) sz cont
+      compile_structured_constant cenv (Const_sort (Sorts.sort_of_univ u)) sz cont
     else
       comp_app compile_structured_constant compile_get_univ cenv
-        (Const_sort (Sorts.Type u)) (Array.of_list s) sz cont
+        (Const_sort (Sorts.sort_of_univ u)) (Array.of_list s) sz cont
 
   | Llet (_id,def,body) ->
       compile_lam env cenv def sz
diff --git a/kernel/constr.ml b/kernel/constr.ml
index c392494e95..57ece320cf 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -129,7 +129,7 @@ let mkRel n = if 0<n && n<=16 then rels.(n-1) else Rel n
 (* Construct a type *)
 let mkProp   = Sort Sorts.prop
 let mkSet    = Sort Sorts.set
-let mkType u = Sort (Sorts.Type u)
+let mkType u = Sort (Sorts.sort_of_univ u)
 let mkSort   = function
   | Sorts.Prop -> mkProp (* Easy sharing *)
   | Sorts.Set -> mkSet
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index f4c2483c14..d14a212de0 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -188,7 +188,7 @@ let instantiate_universes env ctx ar argsorts =
     (* Non singleton type not containing types are interpretable in Set *)
     else if is_type0_univ level then Sorts.set
     (* This is a Type with constraints *)
-    else Sorts.Type level
+    else Sorts.sort_of_univ level
   in
     (ctx, ty)
 
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index a6b48cd7e3..414fc0dc28 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -120,8 +120,8 @@ let mk_sort_accu s u =
   | Prop | Set -> mk_accu (Asort s)
   | Type s ->
      let u = Univ.Instance.of_array u in
-     let s = Univ.subst_instance_universe u s in
-     mk_accu (Asort (Type s))
+     let s = Sorts.sort_of_univ (Univ.subst_instance_universe u s) in
+     mk_accu (Asort s)
 
 let mk_var_accu id = 
   mk_accu (Avar id)
diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index 566dce04c6..e281751be1 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -44,25 +44,25 @@ let compare s1 s2 =
 
 let equal s1 s2 = Int.equal (compare s1 s2) 0
 
+let super = function
+  | Prop | Set -> Type (Universe.type1)
+  | Type u -> Type (Universe.super u)
+
 let is_prop = function
   | Prop -> true
-  | Type u when Universe.equal Universe.type0m u -> true
-  | _ -> false
+  | Set | Type _ -> false
 
 let is_set = function
   | Set -> true
-  | Type u when Universe.equal Universe.type0 u -> true
-  | _ -> false
+  | Prop | Type _ -> false
 
 let is_small = function
   | Prop | Set -> true
-  | Type u -> is_small_univ u
+  | Type _ -> false
 
 let family = function
   | Prop -> InProp
   | Set -> InSet
-  | Type u when is_type0m_univ u -> InProp
-  | Type u when is_type0_univ u -> InSet
   | Type _ -> InType
 
 let family_equal = (==)
diff --git a/kernel/sorts.mli b/kernel/sorts.mli
index 6c5ce4df80..3ca76645db 100644
--- a/kernel/sorts.mli
+++ b/kernel/sorts.mli
@@ -12,7 +12,7 @@
 
 type family = InProp | InSet | InType
 
-type t =
+type t = private
   | Prop
   | Set
   | Type of Univ.Universe.t
@@ -42,6 +42,8 @@ end
 val univ_of_sort : t -> Univ.Universe.t
 val sort_of_univ : Univ.Universe.t -> t
 
+val super : t -> t
+
 val debug_print : t -> Pp.t
 
 val pr_sort_family : family -> Pp.t
diff --git a/kernel/term.ml b/kernel/term.ml
index 58b289eaa5..d791fe67e5 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -19,7 +19,7 @@ open Constr
 type sorts_family = Sorts.family = InProp | InSet | InType
 [@@ocaml.deprecated "Alias for Sorts.family"]
 
-type sorts = Sorts.t =
+type sorts = Sorts.t = private
   | Prop | Set
   | Type of Univ.Universe.t  (** Type *)
 [@@ocaml.deprecated "Alias for Sorts.t"]
diff --git a/kernel/term.mli b/kernel/term.mli
index 181d714ed7..2150f21ed1 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -193,7 +193,7 @@ val kind_of_type : types -> (constr, types) kind_of_type
 type sorts_family = Sorts.family = InProp | InSet | InType
 [@@ocaml.deprecated "Alias for Sorts.family"]
 
-type sorts = Sorts.t =
+type sorts = Sorts.t = private
   | Prop | Set
   | Type of Univ.Universe.t  (** Type *)
 [@@ocaml.deprecated "Alias for Sorts.t"]
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 227a164549..6d12ce3020 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -275,13 +275,13 @@ let sort_of_product env domsort rangsort =
           rangsort
         else
           (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
-          Type (Universe.sup Universe.type0 u1)
+          Sorts.sort_of_univ (Universe.sup Universe.type0 u1)
     (* Product rule (Prop,Type_i,Type_i) *)
-    | (Set,  Type u2)  -> Type (Universe.sup Universe.type0 u2)
+    | (Set,  Type u2)  -> Sorts.sort_of_univ (Universe.sup Universe.type0 u2)
     (* Product rule (Prop,Type_i,Type_i) *)
     | (Prop, Type _)  -> rangsort
     (* Product rule (Type_i,Type_i,Type_i) *)
-    | (Type u1, Type u2) -> Type (Universe.sup u1 u2)
+    | (Type u1, Type u2) -> Sorts.sort_of_univ (Universe.sup u1 u2)
 
 (* [judge_of_product env name (typ1,s1) (typ2,s2)] implements the rule
 
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 9a3eadf747..ac5350e9fa 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -8,7 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 open Names
-open Sorts
 open Univ
 open Constr
 
@@ -335,10 +334,10 @@ let rec whd_accu a stk =
         let args = Array.init (nargs args) (arg args) in
         let s = Obj.obj (Obj.field at 0) in
         begin match s with
-        | Type u ->
+        | Sorts.Type u ->
           let inst = Instance.of_array (Array.map uni_lvl_val args) in
           let u = Univ.subst_instance_universe inst u in
-          Vatom_stk (Asort (Type u), [])
+          Vatom_stk (Asort (Sorts.sort_of_univ u), [])
         | _ -> assert false
         end
      | _ -> assert false