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, 9 insertions, 3 deletions

diff --git a/theories/Logic/ClassicalChoice.v b/theories/Logic/ClassicalChoice.v
index 51f1b3eff..b0301994b 100644
--- a/theories/Logic/ClassicalChoice.v
+++ b/theories/Logic/ClassicalChoice.v
@@ -8,9 +8,15 @@
 
 (*i $Id$ i*)
 
-(** This file provides classical logic, and functional choice *)
-
-(** This file extends ClassicalUniqueChoice.v with the axiom of choice.
+(** This file provides classical logic and functional choice; this
+    especially provides both indefinite descriptions and choice functions
+    but this is weaker than providing epsilon operator and classical logic
+    as the indefinite descriptions provided by the axiom of choice can
+    be used only in a propositional context (especially, they cannot
+    be used to build choice functions outside the scope of a theorem
+    proof) *)
+
+(** This file extends ClassicalUniqueChoice.v with full choice.
     As ClassicalUniqueChoice.v, it implies the double-negation of
     excluded-middle in [Set] and leads to a classical world populated
     with non computable functions. Especially it conflicts with the