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/reduction.ml | 41 +++++++++++++++++++----------------------
 1 file changed, 19 insertions(+), 22 deletions(-)

(limited to 'checker/reduction.ml')

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