Make Sorts.t private

3 files changed, 5 insertions, 7 deletions

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