Remove Sorts.contents

1 files changed, 27 insertions, 34 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 2c61b7a01..3228a155f 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -649,23 +649,19 @@ let check_leq univs u u' =
 let check_sort_cmp_universes env pb s0 s1 univs =
   let open Sorts in
   if not (type_in_type env) then
+    let check_pb u0 u1 =
+      match pb with
+      | CUMUL -> check_leq univs u0 u1
+      | CONV -> check_eq univs u0 u1
+    in
     match (s0,s1) with
-    | (Prop c1, Prop c2) when is_cumul pb ->
-      begin match c1, c2 with
-        | Null, _ | _, Pos -> () (* Prop <= Set *)
-        | _ -> raise NotConvertible
-      end
-    | (Prop c1, Prop c2) -> if c1 != c2 then raise NotConvertible
-    | (Prop c1, Type u) ->
-      let u0 = univ_of_sort s0 in
-      (match pb with
-       | CUMUL -> check_leq univs u0 u
-       | CONV -> check_eq univs u0 u)
-    | (Type u, Prop c) -> raise NotConvertible
-    | (Type u1, Type u2) ->
-      (match pb with
-       | CUMUL -> check_leq univs u1 u2
-       | CONV -> check_eq univs u1 u2)
+    | Prop, Prop | Set, Set -> ()
+    | Prop, (Set | Type _) -> if not (is_cumul pb) then raise NotConvertible
+    | Set, Prop -> raise NotConvertible
+    | Set, Type u -> check_pb Univ.type0_univ u
+    | Type u, Prop -> raise NotConvertible
+    | Type u, Set -> check_pb u Univ.type0_univ
+    | Type u0, Type u1 -> check_pb u0 u1
 
 let checked_sort_cmp_universes env pb s0 s1 univs =
   check_sort_cmp_universes env pb s0 s1 univs; univs
@@ -697,26 +693,23 @@ let infer_leq (univs, cstrs as cuniv) u u' =
       univs, Univ.Constraint.union cstrs cstrs'
 
 let infer_cmp_universes env pb s0 s1 univs =
-  let open Sorts in
-  if type_in_type env then univs
+  if type_in_type env
+  then univs
   else
+    let open Sorts in
+    let infer_pb u0 u1 =
+      match pb with
+      | CUMUL -> infer_leq univs u0 u1
+      | CONV -> infer_eq univs u0 u1
+    in
     match (s0,s1) with
-    | (Prop c1, Prop c2) when is_cumul pb ->
-      begin match c1, c2 with
-        | Null, _ | _, Pos -> univs (* Prop <= Set *)
-        | _ -> raise NotConvertible
-      end
-    | (Prop c1, Prop c2) -> if c1 == c2 then univs else raise NotConvertible
-    | (Prop c1, Type u) ->
-      let u0 = univ_of_sort s0 in
-      (match pb with
-       | CUMUL -> infer_leq univs u0 u
-       | CONV -> infer_eq univs u0 u)
-    | (Type u, Prop c) -> raise NotConvertible
-    | (Type u1, Type u2) ->
-      (match pb with
-       | CUMUL -> infer_leq univs u1 u2
-       | CONV -> infer_eq univs u1 u2)
+    | Prop, Prop | Set, Set -> univs
+    | Prop, (Set | Type _) -> if not (is_cumul pb) then raise NotConvertible else univs
+    | Set, Prop -> raise NotConvertible
+    | Set, Type u -> infer_pb Univ.type0_univ u
+    | Type u, Prop -> raise NotConvertible
+    | Type u, Set -> infer_pb u Univ.type0_univ
+    | Type u0, Type u1 -> infer_pb u0 u1
 
 let infer_convert_instances ~flex u u' (univs,cstrs) =
   let cstrs' =