From 47f840bfac1809e28975e25328b7780cb203f32a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 24 Mar 2004 18:35:06 +0000
Subject: MAJ commentaires

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

diff --git a/theories/Logic/ProofIrrelevance.v b/theories/Logic/ProofIrrelevance.v
index 8636e5ddc5..9a3221ad26 100644
--- a/theories/Logic/ProofIrrelevance.v
+++ b/theories/Logic/ProofIrrelevance.v
@@ -26,7 +26,7 @@
 
     Proof skeleton: classical logic + dependent elimination of
     disjunction + discrimination of proofs implies the existence of a
-    retract from Prop into bool, hence inconsistency by encoding any
+    retract from [Prop] into [bool], hence inconsistency by encoding any
     paradox of system U- (e.g. Hurkens' paradox).
 *)
 
@@ -56,7 +56,7 @@ Hypothesis em : forall A:Prop, or A (~ A).
 Variable B : Prop.
 Variables b1 b2 : B.
 
-(** [p2b] and [b2p] form a retract if [~b1==b2] *)
+(** [p2b] and [b2p] form a retract if [~b1=b2] *)
 
 Definition p2b A := or_elim A (~ A) B (fun _ => b1) (fun _ => b2) (em A).
 Definition b2p b := b1 = b.
@@ -114,5 +114,5 @@ 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 : (A:Prop){A}+{~A}] in CCI
-*)
\ No newline at end of file
+    [bool], we get the inconsistency of [em : forall A:Prop, {A}+{~A}] in CCI
+*)
-- 
cgit v1.2.3