Mise a jour du chapitre library

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

1 files changed, 16 insertions, 15 deletions

diff --git a/doc/Library.tex b/doc/Library.tex
index bb9ef22c1..d9a67061a 100755
--- a/doc/Library.tex
+++ b/doc/Library.tex
@@ -16,29 +16,31 @@
 
 This document is a short description of the \Coq\ standard library.
 This library comes with the system as a complement of the core library
-(the {\bf INIT} library ; see the Reference Manual for a description
+(the {\bf Init} library ; see the Reference Manual for a description
 of this library). It provides a set of modules directly available
 through the \verb!Require! command.
 
 The standard library is composed of the following subdirectories:
 
 \medskip
-\begin{tabular}{lp{10cm}}
-  {\bf LOGIC}   & Classical logic and dependent equality \\
-  {\bf ARITH}   & Basic Peano arithmetic \\
-  {\bf ZARITH}  & Binary integers \\
-  {\bf BOOL}    &  Booleans (basic functions and results) \\
-  {\bf LISTS}   & Monomorphic and polymorphic lists (basic functions and
+\begin{tabular}{lp{12cm}}
+  {\bf Logic}   & Classical logic and dependent equality \\
+  {\bf Arith}   & Basic Peano arithmetic \\
+  {\bf Zarith}  & Basic integer arithmetic \\
+  {\bf Bool}    &  Booleans (basic functions and results) \\
+  {\bf Lists}   & Monomorphic and polymorphic lists (basic functions and
             results), Streams (infinite sequences defined with co-inductive
             types) \\
-  {\bf SETS}    & Sets (classical, constructive, finite, infinite, powerset,
+  {\bf Sets}    & Sets (classical, constructive, finite, infinite, power set,
             etc.) \\
- {\bf RELATIONS} & Relations (definitions and basic results). There is
-             a subdirectory about well-founded relations ({\bf WELLFOUNDED}) \\
- {\bf SORTING}   & Axiomatizations of sorts \\
- {\bf REALS}   & Axiomatization of Real Numbers (classical, basic functions 
-                 and results, integer part and fractional part, require ZARITH
-                 library)
+  {\bf IntMap}    & Representation of finite sets by an efficient
+  structure of map (trees indexed by binary integers).\\
+ {\bf Reals}   & Axiomatization of Real Numbers (classical, basic functions 
+                 and results, integer part and fractional part,
+                 requires the \textbf{Zarith} library).\\
+ {\bf Relations} & Relations (definitions and basic results). \\
+ {\bf Wellfounded} & Well-founded relations (basic results). \\
+
 \end{tabular}
 \medskip
 
@@ -49,7 +51,6 @@ is also a version of this document in HTML format on the WWW, which
 you can access from the \Coq\ home page at
 \texttt{http://pauillac.inria.fr/coq/coq-eng.html}.
 
-
 \input{library/libdoc.tex}
 
 \end{document}