Révision de theories/Logic concernant les axiomes de descriptions.

Mise à jour du tableau des axiomes dans la FAQ.



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

1 files changed, 6 insertions, 5 deletions

diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v
index 51accc4ff..aa65eb44c 100644
--- a/theories/Logic/ClassicalDescription.v
+++ b/theories/Logic/ClassicalDescription.v
@@ -8,12 +8,13 @@
 
 (*i $Id$ i*)
 
-(** This file provides classical logic and definite description *)
+(** This file provides classical logic and definite description, which is
+    equivalent to providing classical logic and Church's iota operator *)
 
-(** Classical definite description operator (i.e. iota) implies
-    excluded-middle in [Set] and leads to a classical world populated
-    with non computable functions. It conflicts with the
-    impredicativity of [Set] *)
+(** Classical logic and definite descriptions implies excluded-middle
+    in [Set] and leads to a classical world populated with non
+    computable functions. It conflicts with the impredicativity of
+    [Set] *)
 
 Set Implicit Arguments.