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

1 files changed, 4 insertions, 3 deletions

diff --git a/theories/Logic/ProofIrrelevance.v b/theories/Logic/ProofIrrelevance.v
index afdc0ffee..7c8869d5d 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.
 *)