MAJ 7.2

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

5 files changed, 13 insertions, 14 deletions

diff --git a/doc/README b/doc/README
index 5a248ea471..b772de3d20 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
-V7.1 is divided into the following documents :
+V7.2 is divided into the following documents :
 
      * Tutorial.ps: An introduction to the use of the Coq Proof Assistant;
 
@@ -14,16 +14,15 @@ V7.1 is divided into the following documents :
      - index on tactics, commands and error messages
 
      * Reference-Manual-addendum.ps, 75 pp., includes more detailed
-      explanations and examples about the following topics:
+       explanations and examples about the following topics:
 
      - the extended Cases (C.Cornes)
      - the Coercions (A. Saļbi)
      - the tactic Omega (P. Crégut)
-     - printing proofs in natural language (Y. Coscoy)
-     - the tactic Ring (S. Boutin and P. Loiseleur)
-     - the Program tactic (C. Parent)
      - the Correctness tactic (J.-C. Filliātre)
-     - the extraction features (J.-C. Filliātre)
+     - the extraction features (J.-C. Filliātre and P. Letouzey) 
+     - the tactic Ring (S. Boutin and P. Loiseleur)
+     - the Setoid_replace tactic (C. Renard)
 
      Index, page and chapter numbers are shared by the two documents, in
      order to make cross-references possible. There is also a on the ftp
@@ -32,8 +31,8 @@ V7.1 is divided into the following documents :
 
      * Library.ps: A description of the Coq standard library;
 
-     * CHANGES: A description of the differences between the
-       versions 6.3.1 and V7.1;
+     * CHANGES: A description of the differences between version 7.2 
+       and previous versions
 
      * rectypes.ps : A tutorial on recursive types by Eduardo Gimenez
 
diff --git a/doc/Tutorial.tex b/doc/Tutorial.tex
index b192e0d0e5..fc22b89bf2 100755
--- a/doc/Tutorial.tex
+++ b/doc/Tutorial.tex
@@ -32,7 +32,7 @@ he does not use any special interface such as Emacs or Centaur.
 Instructions on installation procedures, as well as more comprehensive
 documentation, may be found in the standard distribution of \Coq,
 which may be obtained by anonymous FTP from site \verb:ftp.inria.fr:,
-directory \verb:INRIA/coq/V7.1:. 
+directory \verb:INRIA/coq/V7.2:. 
 
 In the following, all examples preceded by the prompting sequence
 \verb:Coq < : represent user input, terminated by a period. The
@@ -46,7 +46,7 @@ The standard invocation of \Coq\ delivers a message such as:
 \begin{flushleft}
 \begin{verbatim}
 unix:~> coqtop
-Welcome to Coq 7.1 (September 2001)
+Welcome to Coq 7.2 (December 2001)
 
 Coq < 
 \end{verbatim}
diff --git a/doc/cover.html b/doc/cover.html
index b96a099431..0d67ef9ed9 100644
--- a/doc/cover.html
+++ b/doc/cover.html
@@ -19,14 +19,14 @@
 The Coq Proof Assistant<BR><BR>
  Reference Manual<BR></B></FONT><FONT SIZE=7>
 </FONT>
-<BR><BR><FONT SIZE=5><B><BR></B></FONT><FONT SIZE=5><B>Version 7.1</B></FONT><FONT SIZE=5><B>
+<BR><BR><FONT SIZE=5><B><BR></B></FONT><FONT SIZE=5><B>Version 7.2</B></FONT><FONT SIZE=5><B>
 </B></FONT><A NAME="text1"></A><A HREF="node.8.html#note1"><SUP><FONT SIZE=2>1</FONT></SUP></A><FONT SIZE=5><B><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR>
 </B></FONT><FONT SIZE=5><B>The Coq Development Team</B></FONT><FONT SIZE=5><B><BR></B></FONT><FONT SIZE=5><B>LogiCal Project</B></FONT><FONT SIZE=5><B><BR><BR><BR>
 </B></FONT></DIV><BR>
 <BR><BR><BR><BR><BR><BR><BR><BR><BR><BR>
 
 <DIV ALIGN=left>
-<FONT SIZE=4>V7.1,
+<FONT SIZE=4>V7.2,
 </FONT><BR><FONT SIZE=4>©INRIA 1999-2001</FONT><BR></DIV>
 <BR>
 
diff --git a/doc/macros.tex b/doc/macros.tex
index 9841699ef8..f5cfc61937 100755
--- a/doc/macros.tex
+++ b/doc/macros.tex
@@ -2,7 +2,7 @@
 % MACROS FOR THE REFERENCE MANUAL OF COQ %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\newcommand{\coqversion}{7.1}
+\newcommand{\coqversion}{7.2}
 
 % For commentaries (define \com as {} for the release manual)
 %\newcommand{\com}[1]{{\it(* #1 *)}}
diff --git a/doc/title.tex b/doc/title.tex
index 02e02b124e..9f298a3238 100755
--- a/doc/title.tex
+++ b/doc/title.tex
@@ -49,7 +49,7 @@ Action ``Types''}
 \vspace*{520pt}
 \thispagestyle{empty}
 \begin{flushleft}
-{\large{V7.1,
+{\large{V7.2,
 \printingdate}}\\[20pt]
 {\large{\copyright INRIA 1999-2001}}\\
 \end{flushleft}