Cosmetique

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

1 files changed, 7 insertions, 7 deletions

diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
index 12a14f7dc..ff94d8e3b 100644
--- a/theories/Logic/Diaconescu.v
+++ b/theories/Logic/Diaconescu.v
@@ -8,19 +8,19 @@
 
 (*i $Id$ i*)
 
-(* R. Diaconescu [1] showed that the Axiom of Choice in Set Theory
-   entails Excluded-Middle; S. Lacas and B. Werner [2] adapted the proof to
-   show that the axiom of choice in equivalence classes entails
-   Excluded-Middle in Type Theory.
+(* R. Diaconescu [Diaconescu] showed that the Axiom of Choice in Set Theory
+   entails Excluded-Middle; S. Lacas and B. Werner [LacasWerner]
+   adapted the proof to show that the axiom of choice in equivalence
+   classes entails Excluded-Middle in Type Theory.
 
    This is an adaptatation of the proof by Hugo Herbelin to show that
    the relational form of the Axiom of Choice + Extensionality for
    predicates entails Excluded-Middle
 
-   [1] R. Diaconescu, Axiom of Choice and Complementation, in
+   [Diaconescu] R. Diaconescu, Axiom of Choice and Complementation, in
    Proceedings of AMS, vol 51, pp 176-178, 1975.
 
-   [2] S. Lacas, B Werner, Which Choices imply the excluded middle?,
+   [LacasWerner] S. Lacas, B Werner, Which Choices imply the excluded middle?,
    preprint, 1999.
 
 *)
@@ -88,7 +88,7 @@ Qed.
 (* The proof of the excluded middle *)
 (* Remark: P could have been in Set or Type *)
 
-Theorem EM : (P:Prop)P\/~P.
+Theorem pred_ext_and_rel_choice_imp_EM : (P:Prop)P\/~P.
 Proof.
 Intro P.