From 3e96002677226c0cdaa8f355938a76cfb37a722a Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 14 Oct 2010 17:51:11 +0200
Subject: Imported Upstream version 8.3

---
 checker/reduction.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'checker/reduction.ml')

diff --git a/checker/reduction.ml b/checker/reduction.ml
index 9f7dec28..d040c3db 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -154,7 +154,8 @@ type conv_pb =
 
 let sort_cmp univ pb s0 s1 =
   match (s0,s1) with
-    | (Prop c1, Prop c2) -> if c1 = Pos & c2 = Null then raise NotConvertible
+    | (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)  ->
         (match pb with
             CUMUL -> ()
-- 
cgit v1.2.3