From ad00dde8284e9476f98e7ad1ff90c8c95939a50e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 17 Mar 2004 00:11:13 +0000
Subject: Commentaires

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5512 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Logic/ClassicalDescription.v | 2 +-
 theories/Logic/ClassicalFacts.v       | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'theories/Logic')

diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v
index d76d896585..b4d5aedfe5 100644
--- a/theories/Logic/ClassicalDescription.v
+++ b/theories/Logic/ClassicalDescription.v
@@ -29,7 +29,7 @@ Axiom
           exists y : B x, R x y /\ (forall y':B x, R x y' -> y = y')) ->
        exists f : forall x:A, B x, (forall x:A, R x (f x)).
 
-(** Principle of definite description (aka axiom of unique choice) *)
+(** Principle of definite descriptions (aka axiom of unique choice) *)
 
 Theorem description :
  forall (A B:Type) (R:A -> B -> Prop),
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index aa4960a35b..8e1696f872 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -10,8 +10,8 @@
 
 (** Some facts and definitions about classical logic *)
 
-(** [prop_degeneracy] asserts (up to consistency) that there are only *)
-(*  two distinct formulas *)
+(** [prop_degeneracy] (also referred as propositional completeness) *)
+(*  asserts (up to consistency) that there are only two distinct formulas *)
 Definition prop_degeneracy := forall A:Prop, A = True \/ A = False.
 
 (** [prop_extensionality] asserts equivalent formulas are equal *)
@@ -216,4 +216,4 @@ End Proof_irrelevance_CIC.
   satisfy propositional degeneracy without satisfying proof-irrelevance
   (nor dependent case analysis). This would imply that the previous
   results cannot be refined.
-*)
\ No newline at end of file
+*)
-- 
cgit v1.2.3