From 679801623c1f55d0081f952c2094c3572fa39d4f Mon Sep 17 00:00:00 2001
From: glondu
Date: Thu, 23 Sep 2010 10:01:20 +0000
Subject: Fix inconsistency in Prop/Set conversion check

This commit fixes a bug that made the system inconsistent with proof
irrelevance (the main idea being that Set = Prop by reflexivity).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13450 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/reduction.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index d3168a9a17..55a7ca884b 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -183,9 +183,11 @@ type conv_pb =
 
 let sort_cmp pb s0 s1 cuniv =
   match (s0,s1) with
-    | (Prop c1, Prop c2) ->
+    | (Prop c1, Prop c2) when pb = CUMUL ->
         if c1 = Null or c2 = Pos then cuniv   (* Prop <= Set *)
         else raise NotConvertible
+    | (Prop c1, Prop c2) ->
+        if c1 = c2 then cuniv else raise NotConvertible
     | (Prop c1, Type u) when pb = CUMUL -> assert (is_univ_variable u); cuniv
     | (Type u1, Type u2) ->
 	assert (is_univ_variable u2);
-- 
cgit v1.2.3