Library doc adjustments (until page 140)

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

5 files changed, 9 insertions, 9 deletions

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 4dbab94c15..c9052de6c5 100755
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -6,9 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* i$Id$ i*)
+(*i $Id$ i*)
 
-(*** THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED *)
+(*** THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED ***)
 
 Require Le.
 
diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v
index 675a346e22..ae62962ea8 100644
--- a/theories/Lists/ListSet.v
+++ b/theories/Lists/ListSet.v
@@ -10,7 +10,7 @@
 
 (* A Library for finite sets, implemented as lists *)
 (* A Library with similar interface will soon be available under
-  the name TreeSet in the theories/TREES directory *)
+  the name TreeSet in the theories/Trees directory *)
 
 (* PolyList is loaded, but not exported *)
 (* This allow to "hide" the definitions, functions and theorems of PolyList
diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v
index 9dc01f0a1f..16c88e598d 100755
--- a/theories/Lists/Streams.v
+++ b/theories/Lists/Streams.v
@@ -125,11 +125,11 @@ Section Stream_Properties.
 
 Variable P : Stream->Prop.
 
-(*
+(*i
 Inductive   Exists :  Stream -> Prop :=
    Here    : (x:Stream)(P x) ->(Exists x) |
    Further : (x:Stream)~(P x)->(Exists (tl x))->(Exists x).
-*)
+i*)
 
 Inductive   Exists :  Stream -> Prop :=
    Here    : (x:Stream)(P x) ->(Exists x) |
diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v
index 5fbbc93389..a97f549017 100755
--- a/theories/Lists/TheoryList.v
+++ b/theories/Lists/TheoryList.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* Some programs and results about lists following CAML Manual *)
 
diff --git a/theories/Lists/intro.tex b/theories/Lists/intro.tex
index 2930326e19..344bba59ab 100755
--- a/theories/Lists/intro.tex
+++ b/theories/Lists/intro.tex
@@ -1,13 +1,13 @@
 \section{Lists}\label{Lists}
 
-The LISTS library includes the following files:
+This library includes the following files:
 
 \begin{itemize}
 
-\item {\tt Lists.v} THIS OLD LIBRARY IS HERE ONLY FOR COMPATIBILITY
+\item {\tt List.v} THIS OLD LIBRARY IS HERE ONLY FOR COMPATIBILITY
   WITH OLDER VERSIONS OF COQS. THE USER SHOULD USE POLYLIST INSTEAD.
 
-\item {\tt PolyLists.v} contains definitions of (polymorphic) lists, 
+\item {\tt PolyList.v} contains definitions of (polymorphic) lists, 
   functions on lists such as head, tail, map, append and prove some
   properties of these functions. Implicit arguments are used in this
   library, so you should read the Referance Manual about implicit