From d7a7cd2f456f9475cca6dd7666709fe73eaa4d96 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 22 Feb 2002 15:18:31 +0000
Subject: Doc

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2492 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Init/Datatypes.v | 7 ++++---
 1 file 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).
-- 
cgit v1.2.3