MAJ V7.1

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

4 files changed, 25 insertions, 14 deletions

diff --git a/doc/README b/doc/README
index 832e6167c..5a248ea47 100755
--- a/doc/README
+++ b/doc/README
@@ -1,7 +1,7 @@
 You can get the whole documentation of Coq in the tar file all-ps-docs.tar.
 
 You can also get separately each document. The documentation of Coq
-V6.3.1 is divided into the following documents :
+V7.1 is divided into the following documents :
 
      * Tutorial.ps: An introduction to the use of the Coq Proof Assistant;
 
@@ -32,8 +32,8 @@ V6.3.1 is divided into the following documents :
 
      * Library.ps: A description of the Coq standard library;
 
-     * Changes.ps: A description of the differences between the
-       versions V6.3 and V6.3.1;
+     * CHANGES: A description of the differences between the
+       versions 6.3.1 and V7.1;
 
      * rectypes.ps : A tutorial on recursive types by Eduardo Gimenez
 
diff --git a/doc/RefMan-int.tex b/doc/RefMan-int.tex
index 9671c9917..d03b4556d 100755
--- a/doc/RefMan-int.tex
+++ b/doc/RefMan-int.tex
@@ -1,7 +1,7 @@
 \setheaders{Introduction}
 \chapter*{Introduction}
 
-This document is the Reference Manual of version V7.0 of the \Coq\ 
+This document is the Reference Manual of version V7.1 of the \Coq\ 
 proof assistant. A companion volume, the \Coq\ Tutorial, is provided
 for the beginners. It is advised to read the Tutorial first.
 
diff --git a/doc/RefMan-pre.tex b/doc/RefMan-pre.tex
index a60d98dca..95db3e8f9 100755
--- a/doc/RefMan-pre.tex
+++ b/doc/RefMan-pre.tex
@@ -311,9 +311,9 @@ Christine Paulin
 \end{flushright}
 \newpage
 
-\section*{Credits: version 7.0}
+\section*{Credits: versions 7.0 and 7.1}
 
-The current version V7 is a new implementation started in September
+The version V7 is a new implementation started in September
 1999 by J-C. Filliâtre. This is a major revision with respect to the
 internal architecture of the system.
 
@@ -324,28 +324,39 @@ data-structures in order to get more sharing, to prepare the addition
 of modules and also to get closer to a certified kernel.
 
 H. Herbelin introduced a new structure of terms with local
-definitions and redesigned the translation from the high-level
-language of Coq to the internal representation, in particular 
-pattern-matching compiling. 
+definitions. He introduced ``qualified'' names, wrote a new
+pattern-matching compilation algorithm and designed a more compact
+logical consistency check algorithm. He contributed to the
+simplification of Coq internal structures and the optimisation of the
+system.
 
 D. Delahaye introduced a new language for tactics. General tactics
 using pattern-matching on goals and context can directly be written
 from the Coq toplevel. He also provided primitives for the design
 of user-defined tactics in Caml.
 
+M. Mayero contributed the library on real numbers.
+
 J.-C. Filliâtre and P. Letouzey redesigned a new extraction procedure
 from Coq terms to Caml programs. This new extraction procedure, unlike
 the one implemented in previous version of \Coq{} is able
 to handle all terms in the Calculus of Inductive Constructions, 
 even involving universes and strong elimination.
 
-B. Barras improved the reduction strategy for lazy evaluation. 
+B. Barras improved the reduction strategy for lazy evaluation and took care of the logical consistency.
 
 Y. Bertot designed  the \texttt{SearchPattern} and
 \texttt{SearchRewrite} tools and the support for the pcoq interface 
 (\url{http://www-sop.inria.fr/lemme/pcoq/}).
 
-C. Sacerdotti helped by H. Herbelin designed an XML output for the Coq
+M. Mayero and D. Delahaye introduced a decision tactic for commutative fields.
+
+L. Pottier developed a tactic solving linear inequalities on real numbers.
+
+Pierre Crégut developed a new version based on reflexion of the Omega
+decision tactic.
+
+C. Sacerdoti Coen designed an XML output for the Coq
 modules to be used in the Hypertextual Electronic Library of
 Mathematics (HELM cf \url{http://www.cs.unibo.it/helm}).
 
@@ -357,13 +368,13 @@ The development was coordinated by C. Paulin.
 Many discussions within the Démons team and the LogiCal project
 influenced significantly the design of Coq especially with J.
 Chrz\k{a}szcz, J. Courant, P. Courtieu, J. Duprat, J. Goubault, A. Miquel,
-C. Marché, M. Mayero, B. Monate and B. Werner.
+C. Marché, B. Monate and B. Werner.
 
 Intensive users suggested improvements of the system : 
 Y. Bertot, L. Pottier, L. Théry , P. Zimmerman from INRIA 
 C. Alvarado, P. Crégut, J.-F. Monin from France Telecom R \& D.
 \begin{flushright}
-Orsay, Apr. 2001\\
+Orsay, Sep. 2001\\
 Christine Paulin
 \end{flushright}
 \newpage
diff --git a/doc/title.tex b/doc/title.tex
index 28165c0df..02e02b124 100755
--- a/doc/title.tex
+++ b/doc/title.tex
@@ -41,7 +41,7 @@ Action ``Types''}
 \vspace{120pt}
 {\bf #2}\\
 \vfill
-{\Large \bf Coq Development Project}\\
+{\Large \bf LogiCal Project}\\
 \vspace{15pt}
 \end{center}