MAJ 7.2

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

1 files changed, 7 insertions, 8 deletions

diff --git a/doc/README b/doc/README
index 5a248ea47..b772de3d2 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