Commentaires

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4777 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 8 deletions

diff --git a/theories/Logic/ProofIrrelevance.v b/theories/Logic/ProofIrrelevance.v
index 5435ba532..ab2ca17c2 100644
--- a/theories/Logic/ProofIrrelevance.v
+++ b/theories/Logic/ProofIrrelevance.v
@@ -9,10 +9,9 @@
 (*                              May 29th 2002                               *)
 (*                                                                          *)
 (****************************************************************************)
-(*                                Hurkens.v                                 *)
-(****************************************************************************)
-(** This section shows in the pure Calculus of Construction that
-    classical logic + dependent elimination of disjunction entails
+
+(** This is a proof in the pure Calculus of Construction that
+    classical logic in Prop + dependent elimination of disjunction entails
     proof-irrelevance.
 
     Since, dependent elimination is derivable in the Calculus of
@@ -25,10 +24,10 @@
       Calculus of Constructions", Proceedings of Logic in Computer Science
       (LICS'90), 1990.
 
-   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
-   paradox of system U- (e.g. Hurkens' paradox).
+    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
+    paradox of system U- (e.g. Hurkens' paradox).
 *)
 
 Require Hurkens.