Remove Sorts.contents

7 files changed, 16 insertions, 26 deletions

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index bf9e37aa7..5c4cbefad 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -209,8 +209,8 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr)
       match (EConstr.kind !evdref x, EConstr.kind !evdref y) with
       | Sort s, Sort s' ->
         (match ESorts.kind !evdref s, ESorts.kind !evdref s' with
-	| Prop x, Prop y when x == y -> None
-	| Prop _, Type _ -> None
+        | Prop, Prop | Set, Set -> None
+        | (Prop | Set), Type _ -> None
 	| Type x, Type y when Univ.Universe.equal x y -> None (* false *)
 	| _ -> subco ())
       | Prod (name, a, b), Prod (name', a', b') ->
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 2bc603a90..d7118efd7 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -281,8 +281,8 @@ let matches_core env sigma allow_bound_rels
 
         let open Glob_term in
         begin match ps, ESorts.kind sigma s with
-        | GProp, Prop Null -> subst
-        | GSet, Prop Pos -> subst
+        | GProp, Prop -> subst
+        | GSet, Set -> subst
         | GType _, Type _ -> subst
         | _ -> raise PatternMatchingFailure
         end
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 23a985dc3..d0de2f8c0 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -597,8 +597,8 @@ let detype_universe sigma u =
   Univ.Universe.map fn u
 
 let detype_sort sigma = function
-  | Prop Null -> GProp
-  | Prop Pos -> GSet
+  | Prop -> GProp
+  | Set -> GSet
   | Type u ->
     GType
       (if !print_universes
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 8afb9b942..3f5d186d4 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -69,7 +69,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
 	       if onlyalg && alg then
 	         (evdref := Evd.make_flexible_variable !evdref ~algebraic:false l; t)
 	       else t))
-      | Prop Pos when refreshset && not direction ->
+      | Set when refreshset && not direction ->
        (* Cannot make a universe "lower" than "Set",
           only refreshing when we want higher universes. *)
        refresh_sort status ~direction s
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 622a8e982..685aa400b 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -150,8 +150,8 @@ let pattern_of_constr env sigma t =
     | Rel n  -> PRel n
     | Meta n -> PMeta (Some (Id.of_string ("META" ^ string_of_int n)))
     | Var id -> PVar id
-    | Sort (Prop Null) -> PSort GProp
-    | Sort (Prop Pos) -> PSort GSet
+    | Sort Prop -> PSort GProp
+    | Sort Set -> PSort GSet
     | Sort (Type _) -> PSort (GType [])
     | Cast (c,_,_)      -> pattern_of_constr env c
     | LetIn (na,c,t,b) -> PLetIn (na,pattern_of_constr env c,Some (pattern_of_constr env t),
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 746a68b21..7e43c5e41 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -149,18 +149,13 @@ let retype ?(polyprop=true) sigma =
     | Cast (c,_, s) when isSort sigma s -> destSort sigma s
     | Sort s ->
       begin match ESorts.kind sigma s with
-      | Prop _ -> Sorts.type1
+      | Prop | Set -> Sorts.type1
       | Type u -> Type (Univ.super u)
       end
     | Prod (name,t,c2) ->
-        (match (sort_of env t, sort_of (push_rel (LocalAssum (name,t)) env) c2) with
-	  | _, (Prop Null as s) -> s
-          | Prop _, (Prop Pos as s) -> s
-          | Type _, (Prop Pos as s) when is_impredicative_set env -> s
-          | Type u1, Prop Pos -> Type (Univ.sup u1 Univ.type0_univ)
-	  | Prop Pos, (Type u2) -> Type (Univ.sup Univ.type0_univ u2)
-	  | Prop Null, (Type _ as s) -> s
-	  | Type u1, Type u2 -> Type (Univ.sup u1 u2))
+      let dom = sort_of env t in
+      let rang = sort_of (push_rel (LocalAssum (name,t)) env) c2 in
+      Typeops.sort_of_product env dom rang
     | App(f,args) when is_template_polymorphic env sigma f ->
       let t = type_of_global_reference_knowing_parameters env f args in
         sort_of_atomic_type env sigma t args
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index cf34ac016..a66ecaaac 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -241,10 +241,6 @@ let judge_of_set =
   { uj_val = EConstr.mkSet;
     uj_type = EConstr.mkSort Sorts.type1 }
 
-let judge_of_prop_contents = function
-  | Null -> judge_of_prop
-  | Pos -> judge_of_set
-
 let judge_of_type u =
   let uu = Univ.Universe.super u in
     { uj_val = EConstr.mkType u;
@@ -333,10 +329,9 @@ let rec execute env sigma cstr =
 
     | Sort s ->
       begin match ESorts.kind sigma s with
-      | Prop c ->
-        sigma, judge_of_prop_contents c
-      | Type u ->
-        sigma, judge_of_type u
+        | Prop -> sigma, judge_of_prop
+        | Set -> sigma, judge_of_set
+        | Type u -> sigma, judge_of_type u
       end
 
     | Proj (p, c) ->