Remove Sorts.contents

8 files changed, 53 insertions, 61 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index a890f2cef..4846a9af8 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -33,11 +33,10 @@ open Names
 
 (** {6 The sorts of CCI. } *)
 
-type contents = Pos | Null
-
 type sorts =
-  | Prop of contents       (** Prop and Set *)
-  | Type of Univ.universe  (** Type *)
+  | Prop
+  | Set
+  | Type of Univ.universe
 
 (** {6 The sorts family of CCI. } *)
 
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 916934a81..bcb71fe55 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -107,11 +107,11 @@ let rec sorts_of_constr_args env t =
 
 (* Prop and Set are small *)
 let is_small_sort = function
-  | Prop _ -> true
+  | Prop | Set -> true
   | _ -> false
 
 let is_logic_sort = function
-| Prop Null -> true
+| Prop -> true
 | _ -> false
 
 (* [infos] is a sequence of pair [islogic,issmall] for each type in
@@ -186,10 +186,10 @@ let check_predicativity env s small level =
         (*     (universes env) in *)
         if not (Univ.check_leq (universes env) level u) then
           failwith "impredicative Type inductive type"
-    | Prop Pos, ImpredicativeSet -> ()
-    | Prop Pos, _ ->
+    | Set, ImpredicativeSet -> ()
+    | Set, _ ->
         if not small then failwith "impredicative Set inductive type"
-    | Prop Null,_ -> ()
+    | Prop,_ -> ()
 
 
 let sort_of_ind = function
diff --git a/checker/inductive.ml b/checker/inductive.ml
index e1c6b135d..b1edec556 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -101,7 +101,7 @@ let instantiate_params full t u args sign =
   substl subs ty
 
 let full_inductive_instantiate mib u params sign =
-  let dummy = Prop Null in
+  let dummy = Prop in
   let t = mkArity (Term.subst_instance_context u sign,dummy) in
     fst (destArity (instantiate_params true t u params mib.mind_params_ctxt))
 
@@ -137,8 +137,8 @@ Remark: Set (predicative) is encoded as Type(0)
 
 let sort_as_univ = function
 | Type u -> u
-| Prop Null -> Univ.type0m_univ
-| Prop Pos -> Univ.type0_univ
+| Prop -> Univ.type0m_univ
+| Set -> Univ.type0_univ
 
 (* cons_subst add the mapping [u |-> su] in subst if [u] is not *)
 (* in the domain or add [u |-> sup x su] if [u] is already mapped *)
@@ -195,9 +195,9 @@ let instantiate_universes env ctx ar argsorts =
   let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in
   let ty =
     (* Singleton type not containing types are interpretable in Prop *)
-    if Univ.is_type0m_univ level then Prop Null
+    if Univ.is_type0m_univ level then Prop
     (* Non singleton type not containing types are interpretable in Set *)
-    else if Univ.is_type0_univ level then Prop Pos
+    else if Univ.is_type0_univ level then Set
     (* This is a Type with constraints *)
     else Type level
   in
@@ -226,8 +226,8 @@ let type_of_inductive env mip =
 (* The max of an array of universes *)
 
 let cumulate_constructor_univ u = function
-  | Prop Null -> u
-  | Prop Pos -> Univ.sup Univ.type0_univ u
+  | Prop -> u
+  | Set -> Univ.sup Univ.type0_univ u
   | Type u' -> Univ.sup u u'
 
 let max_inductive_sort =
diff --git a/checker/print.ml b/checker/print.ml
index fc9cd687e..247c811f8 100644
--- a/checker/print.ml
+++ b/checker/print.ml
@@ -57,8 +57,8 @@ let print_pure_constr fmt csr =
     fprintf fmt "Proj(%a,@,@[%a@])" sp_con_display (Projection.constant p) pp_term c
 
   and pp_sort fmt = function
-    | Prop(Pos) -> pp_print_string fmt  "Set"
-    | Prop(Null) -> pp_print_string fmt "Prop"
+    | Set -> pp_print_string fmt  "Set"
+    | Prop -> pp_print_string fmt "Prop"
     | Type u -> fprintf fmt "Type(%a)" chk_pp (Univ.pr_uni u)
 
   and pp_name fmt = function
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 4e508dc77..16c701213 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -210,29 +210,26 @@ let convert_constructors
 
 let sort_cmp env univ pb s0 s1 =
   match (s0,s1) with
-    | (Prop c1, Prop c2) when pb = CUMUL -> if c1 = Pos && c2 = Null then raise NotConvertible
-    | (Prop c1, Prop c2) -> if c1 <> c2 then raise NotConvertible
-    | (Prop c1, Type u)  ->
+  | Prop, Prop | Set, Set -> ()
+  | Prop, (Set | Type _) | Set, Type _ ->
+    if not (pb = CUMUL) then raise NotConvertible
+  | Type u1, Type u2 ->
+    (** FIXME: handle type-in-type option here *)
+    if (* snd (engagement env) == StratifiedType && *)
+      not
         (match pb with
-            CUMUL -> ()
-          | _ -> raise NotConvertible)
-    | (Type u1, Type u2) ->
-        (** FIXME: handle type-in-type option here *)
-        if (* snd (engagement env) == StratifiedType && *)
-          not
-	  (match pb with
-            | CONV -> Univ.check_eq univ u1 u2
-	    | CUMUL -> Univ.check_leq univ u1 u2)
-        then begin
-          if !Flags.debug then begin
-            let op = match pb with CONV -> "=" | CUMUL -> "<=" in
-            Format.eprintf "sort_cmp: @[%a@]\n%!" Pp.pp_with Pp.(
-               str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut()
-               ++ Univ.pr_universes univ)
-          end;
-          raise NotConvertible
-        end
-    | (_, _) -> raise NotConvertible
+         | CONV -> Univ.check_eq univ u1 u2
+         | CUMUL -> Univ.check_leq univ u1 u2)
+    then begin
+      if !Flags.debug then begin
+        let op = match pb with CONV -> "=" | CUMUL -> "<=" in
+        Format.eprintf "sort_cmp: @[%a@]\n%!" Pp.pp_with Pp.(
+            str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut()
+            ++ Univ.pr_universes univ)
+      end;
+      raise NotConvertible
+    end
+  | Set, Prop | Type _, (Prop | Set) -> raise NotConvertible
 
 let rec no_arg_available = function
   | [] -> true
diff --git a/checker/term.ml b/checker/term.ml
index 509634bdb..d84491b38 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -20,15 +20,15 @@ open Cic
 (* Sorts. *)
 
 let family_of_sort = function
-  | Prop Null -> InProp
-  | Prop Pos -> InSet
+  | Prop -> InProp
+  | Set -> InSet
   | Type _ -> InType
 
 let family_equal = (==)
 
 let sort_of_univ u =
-  if Univ.is_type0m_univ u then Prop Null
-  else if Univ.is_type0_univ u then Prop Pos
+  if Univ.is_type0m_univ u then Prop
+  else if Univ.is_type0_univ u then Set
   else Type u
 
 (********************************************************************)
@@ -356,15 +356,11 @@ let rec isArity c =
 (* alpha conversion : ignore print names and casts *)
 
 let compare_sorts s1 s2 = match s1, s2 with
-| Prop c1, Prop c2 ->
-  begin match c1, c2 with
-  | Pos, Pos | Null, Null -> true
-  | Pos, Null -> false
-  | Null, Pos -> false
-  end
+| Prop, Prop | Set, Set -> true
 | Type u1, Type u2 -> Univ.Universe.equal u1 u2
-| Prop _, Type _ -> false
-| Type _, Prop _ -> false
+| Prop, Set | Set, Prop -> false
+| (Prop | Set), Type _ -> false
+| Type _, (Prop | Set) -> false
 
 let eq_puniverses f (c1,u1) (c2,u2) =
   Univ.Instance.equal u1 u2 && f c1 c2
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 345ee5b8f..19ede4b9a 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -103,11 +103,11 @@ let judge_of_apply env (f,funj) argjv =
 let sort_of_product env domsort rangsort =
   match (domsort, rangsort) with
     (* Product rule (s,Prop,Prop) *)
-    | (_,       Prop Null)  -> rangsort
+    | _,       Prop  -> rangsort
     (* Product rule (Prop/Set,Set,Set) *)
-    | (Prop _,  Prop Pos) -> rangsort
+    | (Prop | Set),  Set -> rangsort
     (* Product rule (Type,Set,?) *)
-    | (Type u1, Prop Pos) ->
+    | Type u1, Set ->
         if engagement env = ImpredicativeSet then
           (* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
           rangsort
@@ -115,11 +115,11 @@ let sort_of_product env domsort rangsort =
           (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
           Type (Univ.sup u1 Univ.type0_univ)
     (* Product rule (Prop,Type_i,Type_i) *)
-    | (Prop Pos,  Type u2)  -> Type (Univ.sup Univ.type0_univ u2)
+    | Set,  Type u2  -> Type (Univ.sup Univ.type0_univ u2)
     (* Product rule (Prop,Type_i,Type_i) *)
-    | (Prop Null, Type _)  -> rangsort
+    | Prop, Type _  -> rangsort
     (* Product rule (Type_i,Type_i,Type_i) *)
-    | (Type u1, Type u2) -> Type (Univ.sup u1 u2)
+    | Type u1, Type u2 -> Type (Univ.sup u1 u2)
 
 (* Type of a type cast *)
 
@@ -239,7 +239,7 @@ let type_fixpoint env lna lar lbody vdefj =
 let rec execute env cstr =
   match cstr with
     (* Atomic terms *)
-    | Sort (Prop _) -> judge_of_prop
+    | Sort (Prop | Set) -> judge_of_prop
 
     | Sort (Type u) -> judge_of_type u
 
diff --git a/checker/values.ml b/checker/values.ml
index 4f28d6e44..88cdb644d 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -15,7 +15,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 42fb0781dc5f7f2cbe3ca127f8249264 checker/cic.mli
+MD5 c395aa2dbfc18794b3b7192f3dc5b2e5 checker/cic.mli
 
 *)
 
@@ -122,7 +122,7 @@ let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|]
 
 (** kernel/term *)
 
-let v_sort = v_sum "sort" 0 [|[|v_enum "cnt" 2|];[|v_univ|]|]
+let v_sort = v_sum "sort" 2 (*Prop, Set*) [|[|v_univ(*Type*)|]|]
 let v_sortfam = v_enum "sorts_family" 3
 
 let v_puniverses v = v_tuple "punivs" [|v;v_instance|]