MAJ nouvelles théories

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

1 files changed, 18 insertions, 16 deletions

diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex
index 6c28fbb336..65eab3b742 100644
--- a/doc/refman/RefMan-lib.tex
+++ b/doc/refman/RefMan-lib.tex
@@ -16,9 +16,9 @@ The \Coq\ library is structured into three parts:
   (see section~\ref{Require});
 
 \item[User contributions:] Other specification and proof developments
-  coming from the \Coq\ users' community. These libraries are no
-  longer distributed with the system.  They are available by anonymous
-  FTP (see section~\ref{Contributions}).
+  coming from the \Coq\ users' community. These libraries are
+  available for download at \texttt{http://coq.inria.fr} (see
+  section~\ref{Contributions}).
 \end{description}
 
 This chapter briefly reviews these libraries.
@@ -27,8 +27,8 @@ This chapter briefly reviews these libraries.
 \label{Prelude}
 
 This section lists the basic notions and results which are directly
-available in the standard \Coq\ system
-\footnote{Most of these constructions are defined in the
+available in the standard \Coq\ system\footnote{Most 
+of these constructions are defined in the
 {\tt Prelude} module in directory {\tt theories/Init} at the {\Coq}
 root directory; this includes the modules
 {\tt Notations},
@@ -155,6 +155,7 @@ Section Projections.
 Variables A B : Prop.
 Theorem proj1 : A /\ B -> A.
 Theorem proj2 : A /\ B -> B.
+End Projections.
 \end{coq_example*}
 \begin{coq_eval}
 Abort All.
@@ -165,7 +166,6 @@ Abort All.
 \ttindex{iff}
 \ttindex{IF\_then\_else}
 \begin{coq_example*}
-End Projections.
 Inductive or (A B:Prop) : Prop :=
   | or_introl (_:A)
   | or_intror (_:B).
@@ -800,22 +800,24 @@ subdirectories:
 \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 NArith}  & Basic positive integer arithmetic \\
+  {\bf ZArith}  & Basic relative 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, power set,
             etc.) \\
-  {\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, 
-                 integer part, fractional part, limit, derivative, Cauchy 
-                 series, power series and results,... Requires the 
-                 \textbf{ZArith} library).\\
+  {\bf FSets}   & Specification and implementations of finite sets and finite
+                  maps (by lists and by AVL trees)\\
+  {\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, 
+                  integer part, fractional part, limit, derivative, Cauchy 
+                  series, power series and results,...)\\
  {\bf Relations} & Relations (definitions and basic results). \\
- {\bf Sorting} & Sorted list (basic definitions and heapsort correctness). \\
- {\bf Strings} & 8-bits characters and strings\\
+ {\bf Sorting}  & Sorted list (basic definitions and heapsort correctness). \\
+ {\bf Strings}  & 8-bits characters and strings\\
  {\bf Wellfounded} & Well-founded relations (basic results). \\
 
 \end{tabular}