From af0a04b8e16c2554e0c747da6d625799b332f5fe Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Wed, 11 Oct 2017 19:41:23 +0200
Subject: Remove Sorts.contents

---
 checker/indtypes.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'checker/indtypes.ml')

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
-- 
cgit v1.2.3