MAJ

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

1 files changed, 3 insertions, 4 deletions

diff --git a/doc/Library.tex b/doc/Library.tex
index c66b6e1cf1..35fda3ff77 100755
--- a/doc/Library.tex
+++ b/doc/Library.tex
@@ -32,15 +32,14 @@ The standard library is composed of the following subdirectories:
   {\bf Bool}    & Booleans (basic functions and results) \\
   {\bf Arith}   & Basic Peano arithmetic \\
   {\bf ZArith}  & Basic integer arithmetic \\
-  {\bf Reals}   & Axiomatization of Real Numbers (classical, basic functions 
-                  and results, integer part and fractional part,
-                  requires the \textbf{ZArith} library).\\
+  {\bf Reals}   & Classical Real Numbers and Analysis \\
   {\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, power set,
                   etc.) \\
   {\bf Relations}   & Relations (definitions and basic results). \\
+  {\bf Sorting}  & Sorted list (basic definitions and heapsort correctness). \\
   {\bf Wellfounded} & Well-founded relations (basic results). \\
   {\bf IntMap}      & Representation of finite sets by an efficient
                       structure of map (trees indexed by binary integers).\\
@@ -53,7 +52,7 @@ specifications ({\sf Gallina} files) have
 been roughly, and automatically, pasted in the following pages. There
 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}.
+\texttt{http://coq.inria.fr/library}.
 
 \input{library.coqweb.tex}