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

---
 engine/evd.ml     |  2 +-
 engine/namegen.ml |  5 +++--
 engine/termops.ml | 15 +++++++--------
 3 files changed, 11 insertions(+), 11 deletions(-)

(limited to 'engine')

diff --git a/engine/evd.ml b/engine/evd.ml
index 714a0b645..ea9c0eee2 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -852,7 +852,7 @@ let normalize_universe_instance evd l =
 
 let normalize_sort evars s =
   match s with
-  | Prop _ -> s
+  | Prop | Set -> s
   | Type u -> 
     let u' = normalize_universe evars u in
     if u' == u then s else Type u'
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 23c691139..978f33b68 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -137,8 +137,9 @@ let lowercase_first_char id = (* First character of a constr *)
         s ^ Unicode.lowercase_first_char s'
 
 let sort_hdchar = function
-  | Prop(_) -> "P"
-  | Type(_) -> "T"
+  | Prop -> "P"
+  | Set -> "S"
+  | Type _ -> "T"
 
 let hdchar env sigma c =
   let rec hdrec k c =
diff --git a/engine/termops.ml b/engine/termops.ml
index 2db2e07bf..2b179c43b 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -25,8 +25,8 @@ module CompactedDecl = Context.Compacted.Declaration
 (* Sorts and sort family *)
 
 let print_sort = function
-  | Prop Pos -> (str "Set")
-  | Prop Null -> (str "Prop")
+  | Set -> (str "Set")
+  | Prop -> (str "Prop")
   | Type u -> (str "Type(" ++ Univ.Universe.pr u ++ str ")")
 
 let pr_sort_family = function
@@ -1162,15 +1162,14 @@ let is_template_polymorphic env sigma f =
 
 let base_sort_cmp pb s0 s1 =
   match (s0,s1) with
-    | (Prop c1, Prop c2) -> c1 == Null || c2 == Pos  (* Prop <= Set *)
-    | (Prop c1, Type u)  -> pb == Reduction.CUMUL
-    | (Type u1, Type u2) -> true
-    | _ -> false
+  | Prop, Prop | Set, Set | Type _, Type _ -> true
+  | Prop, Set | Prop, Type _ | Set, Type _ -> pb == Reduction.CUMUL
+  | Set, Prop | Type _, Prop | Type _, Set -> false
 
 let rec is_Prop sigma c = match EConstr.kind sigma c with
   | Sort u ->
     begin match EConstr.ESorts.kind sigma u with
-    | Prop Null -> true
+    | Prop -> true
     | _ -> false
     end
   | Cast (c,_,_) -> is_Prop sigma c
@@ -1179,7 +1178,7 @@ let rec is_Prop sigma c = match EConstr.kind sigma c with
 let rec is_Set sigma c = match EConstr.kind sigma c with
   | Sort u ->
     begin match EConstr.ESorts.kind sigma u with
-    | Prop Pos -> true
+    | Set -> true
     | _ -> false
     end
   | Cast (c,_,_) -> is_Set sigma c
-- 
cgit v1.2.3