From be9d9d2b0c2569df032776896977c8cdf5e37f66 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 7 Nov 2004 08:48:10 +0000
Subject: MAJ commentaire sur incohérence EM dans Set

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6281 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Logic/ProofIrrelevance.v | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/theories/Logic/ProofIrrelevance.v b/theories/Logic/ProofIrrelevance.v
index afdc0ffee3..7c8869d5d8 100644
--- a/theories/Logic/ProofIrrelevance.v
+++ b/theories/Logic/ProofIrrelevance.v
@@ -108,7 +108,8 @@ Proof
 
 End Proof_irrelevance_CCI.
 
-(** Remark: in CCI, [bool] can be taken in [Set] as well in the
-    paradox and since [~true=false] for [true] and [false] in
-    [bool], we get the inconsistency of [em : forall A:Prop, {A}+{~A}] in CCI
+(** Remark: in the Set-impredicative CCI, Hurkens' paradox still holds with
+    [bool] in [Set] and since [~true=false] for [true] and [false]
+    in [bool] from [Set], we get the inconsistency of
+    [em : forall A:Prop, {A}+{~A}] in the Set-impredicative CCI.
 *)
-- 
cgit v1.2.3