Doc

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

1 files changed, 4 insertions, 3 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 5b23435ff0..9f72b6e174 100755
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -25,12 +25,13 @@ Add Printing If bool.
 Inductive nat : Set := O : nat 
                      | S : nat->nat.
 
-(** [Empty_set] has no inhabitants *)
+(** [Empty_set] has no inhabitant *)
 
 Inductive Empty_set:Set :=.
 
-(** [identity A a] is a singleton datatype containing only [a] of type [A];
-    the sole inhabitant is denoted [refl_identity A a] *)
+(** [identity A a] is the family of datatypes on [A] whose sole non-empty
+    member is the singleton datatype [identity A a a] whose
+    sole inhabitant is denoted [refl_identity A a] *)
 
 Inductive identity [A:Set; a:A] : A->Set :=
      refl_identity: (identity A a a).