Make Sorts.t private

21 files changed, 44 insertions, 45 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 8756ebfdf2..c7b092b114 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -50,7 +50,7 @@ let in_punivs a = (a, EInstance.empty)
 
 let mkProp = of_kind (Sort (ESorts.make Sorts.prop))
 let mkSet = of_kind (Sort (ESorts.make Sorts.set))
-let mkType u = of_kind (Sort (ESorts.make (Sorts.Type u)))
+let mkType u = of_kind (Sort (ESorts.make (Sorts.sort_of_univ u)))
 let mkRel n = of_kind (Rel n)
 let mkVar id = of_kind (Var id)
 let mkMeta n = of_kind (Meta n)
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 840c14b241..5c2b480db4 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -836,7 +836,7 @@ let occur_evar_upto sigma n c =
 let judge_of_new_Type evd =
   let open EConstr in
   let (evd', s) = new_univ_variable univ_rigid evd in
-  (evd', { uj_val = mkSort (Sorts.Type s); uj_type = mkSort (Sorts.Type (Univ.super s)) })
+  (evd', { uj_val = mkType s; uj_type = mkType (Univ.super s) })
 
 let subterm_source evk ?where (loc,k) =
   let evk = match k with
diff --git a/engine/evd.ml b/engine/evd.ml
index dd2be29bd9..b8c52b27df 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -898,7 +898,7 @@ let new_univ_variable ?loc ?name rigid evd =
 
 let new_sort_variable ?loc ?name rigid d =
   let (d', u) = new_univ_variable ?loc rigid ?name d in
-    (d', Type u)
+    (d', Sorts.sort_of_univ u)
 
 let add_global_univ d u =
   { d with universes = UState.add_global_univ d.universes u }
@@ -965,7 +965,7 @@ let normalize_sort evars s =
   | Prop | Set -> s
   | Type u -> 
     let u' = normalize_universe evars u in
-    if u' == u then s else Type u'
+    if u' == u then s else Sorts.sort_of_univ u'
 
 (* FIXME inefficient *)
 let set_eq_sort env d s1 s2 =
diff --git a/engine/univGen.ml b/engine/univGen.ml
index 40c4c909fe..4ad7fccb3a 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -28,7 +28,7 @@ let fresh_level () =
 (* TODO: remove *)
 let new_univ () = Univ.Universe.make (fresh_level ())
 let new_Type () = mkType (new_univ ())
-let new_Type_sort () = Type (new_univ ())
+let new_Type_sort () = sort_of_univ (new_univ ())
 
 let fresh_instance auctx =
   let inst = Array.init (AUContext.size auctx) (fun _ -> fresh_level()) in
@@ -132,7 +132,7 @@ let fresh_sort_in_family = function
   | InSet -> Sorts.set, ContextSet.empty
   | InType ->
     let u = fresh_level () in
-      Type (Univ.Universe.make u), ContextSet.singleton u
+      sort_of_univ (Univ.Universe.make u), ContextSet.singleton u
 
 let new_sort_in_family sf =
   fst (fresh_sort_in_family sf)
diff --git a/interp/discharge.ml b/interp/discharge.ml
index 353b0f6057..524bf9a002 100644
--- a/interp/discharge.ml
+++ b/interp/discharge.ml
@@ -69,7 +69,7 @@ let refresh_polymorphic_type_of_inductive (_,mip) =
   | RegularArity s -> s.mind_user_arity, false
   | TemplateArity ar ->
     let ctx = List.rev mip.mind_arity_ctxt in
-      mkArity (List.rev ctx, Type ar.template_level), true
+      mkArity (List.rev ctx, Sorts.sort_of_univ ar.template_level), true
 
 let process_inductive info modlist mib =
   let section_decls = Lib.named_of_variable_context info.Lib.abstr_ctx in
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
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index a62427834d..55dfdc0574 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -97,7 +97,7 @@ let define_pure_evar_as_product evd evk =
           new_type_evar newenv evd1 status ~src ~filter
         in
 	let prods = Univ.sup (univ_of_sort u1) (univ_of_sort srng) in
-	let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) (ESorts.kind evd1 s) in
+        let evd3 = Evd.set_leq_sort evenv evd3 (Sorts.sort_of_univ prods) (ESorts.kind evd1 s) in
 	  evd3, rng
   in
   let prod = mkProd (Name id, dom, subst_var id rng) in
@@ -164,13 +164,12 @@ let rec evar_absorb_arguments env evd (evk,args as ev) = function
 (* Refining an evar to a sort *)
 
 let define_evar_as_sort env evd (ev,args) =
-  let evd, u = new_univ_variable univ_rigid evd in
+  let evd, s = new_sort_variable univ_rigid evd in
   let evi = Evd.find_undefined evd ev in 
-  let s = Type u in
   let concl = Reductionops.whd_all (evar_env evi) evd evi.evar_concl in
   let sort = destSort evd concl in
   let evd' = Evd.define ev (mkSort s) evd in
-  Evd.set_leq_sort env evd' (Type (Univ.super u)) (ESorts.kind evd' sort), s
+  Evd.set_leq_sort env evd' (Sorts.super s) (ESorts.kind evd' sort), s
 
 (* Propagation of constraints through application and abstraction:
    Given a type constraint on a functional term, returns the type
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 9612932439..ae1b4af3c3 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -29,7 +29,6 @@ open Util
 open Names
 open Evd
 open Constr
-open Term
 open Termops
 open Environ
 open EConstr
@@ -448,7 +447,7 @@ let pretype_ref ?loc sigma env ref us =
 let judge_of_Type ?loc evd s =
   let evd, s = interp_universe ?loc evd s in
   let judge = 
-    { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }
+    { uj_val = mkType s; uj_type = mkType (Univ.super s) }
   in
     evd, judge
 
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index a76a203e37..fd3c77338c 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -151,7 +151,7 @@ let retype ?(polyprop=true) sigma =
     | Sort s ->
       begin match ESorts.kind sigma s with
       | Prop | Set -> Sorts.type1
-      | Type u -> Type (Univ.super u)
+      | Type u -> Sorts.sort_of_univ (Univ.super u)
       end
     | Prod (name,t,c2) ->
       let dom = sort_of env t in
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 3c1115d056..5dd55b8a9f 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -789,7 +789,7 @@ let build_congr env (eq,refl,ctx) ind =
   let ctx = (fst ctx, Univ.enforce_leq uni (univ_of_eq env eq) (snd ctx)) in
   let c = 
   my_it_mkLambda_or_LetIn paramsctxt
-     (mkNamedLambda varB (mkSort (Type uni))
+     (mkNamedLambda varB (mkType uni)
      (mkNamedLambda varf (mkArrow (lift 1 ty) (mkVar varB))
      (my_it_mkLambda_or_LetIn_name (lift_rel_context 2 realsign)
      (mkNamedLambda varH
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 7fa99b25cb..e71946e8b8 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -140,7 +140,7 @@ let make_conclusion_flexible sigma = function
      | _ -> sigma)
 
 let is_impredicative env u =
-  u = Prop || (is_impredicative_set env && u = Set)
+  Sorts.is_prop u || (is_impredicative_set env && Sorts.is_set u)
 
 let interp_ind_arity env sigma ind =
   let c = intern_gen IsType env sigma ind.ind_arity in
@@ -260,7 +260,7 @@ let solve_constraints_system levels level_bounds =
 let inductive_levels env evd poly arities inds =
   let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in
   let levels = List.map (fun (x,(ctx,a)) ->
-    if a = Prop then None
+    if Sorts.is_prop a then None
     else Some (univ_of_sort a)) destarities
   in
   let cstrs_levels, min_levels, sizes =
@@ -313,16 +313,16 @@ let inductive_levels env evd poly arities inds =
            (* "Polymorphic" type constraint and more than one constructor,
                should not land in Prop. Add constraint only if it would
                land in Prop directly (no informative arguments as well). *)
-            Evd.set_leq_sort env evd Set du
+            Evd.set_leq_sort env evd Sorts.set du
           else evd
         in
         let duu = Sorts.univ_of_sort du in
         let evd =
           if not (Univ.is_small_univ duu) && Univ.Universe.equal cu duu then
             if is_flexible_sort evd duu && not (Evd.check_leq evd Univ.type0_univ duu) then
-              Evd.set_eq_sort env evd Prop du
+              Evd.set_eq_sort env evd Sorts.prop du
             else evd
-          else Evd.set_eq_sort env evd (Type cu) du
+          else Evd.set_eq_sort env evd (sort_of_univ cu) du
         in
           (evd, arity :: arities))
     (evd,[]) (Array.to_list levels') destarities sizes
diff --git a/vernac/record.ml b/vernac/record.ml
index 3202c9bed2..9f5658ecbd 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -167,12 +167,12 @@ let typecheck_params_and_fields finite def poly pl ps records =
 	(Sorts.is_set sort && is_impredicative_set env0)) then
         sigma, typ
       else
-        let sigma = Evd.set_leq_sort env_ar sigma (Type univ) sort in
-	if Univ.is_small_univ univ &&
+        let sigma = Evd.set_leq_sort env_ar sigma (Sorts.sort_of_univ univ) sort in
+        if Univ.is_small_univ univ &&
            Option.cata (Evd.is_flexible_level sigma) false (Evd.is_sort_variable sigma sort) then
 	   (* We can assume that the level in aritysort is not constrained
 	       and clear it, if it is flexible *)
-   Evd.set_eq_sort env_ar sigma Set sort, EConstr.mkSort (Sorts.sort_of_univ univ)
+   Evd.set_eq_sort env_ar sigma Sorts.set sort, EConstr.mkSort (Sorts.sort_of_univ univ)
         else sigma, typ
   in
   let (sigma, typs) = List.fold_left2_map fold sigma typs data in