MAJ

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

1 files changed, 6 insertions, 11 deletions

diff --git a/ANNONCE b/ANNONCE
index c9ff7c49b..a3138749f 100644
--- a/ANNONCE
+++ b/ANNONCE
@@ -17,8 +17,7 @@ quantification and notations for standard arithmetical notions
 (e.g. +, *, <, <=) without conflicts with the rest of the syntax. A new
 notion of "interpretation scopes" allows also to reuse the same
 notations in different contexts of formalisation (e.g. +, * are valid
-on nat, Z, R, types, etc). The new syntax, with explanatory examples,
-is described in document ??? from the distribution.
+on nat, Z, R, types, etc).
 
   Thirdly, the standard library has been revised and simplified. There
 is now only one equality "=" and one existential quantification valid
@@ -27,9 +26,8 @@ been re-organised. The basic notions from the initial state now have
 implicit arguments.
 
   Coq version 8.0 comes with a smart and robust comment-preserving
-automatic translator from old to new syntax. Follow the instructions
-in document ??? from the distribution to update your developments from
-old to new syntax.
+automatic translator from old to new syntax. A translation package
+with a documentation of the new syntax accompanies the distribution.
 
   Coq version 8.0 brings also a new automation tactic for first-order
 statements and various improvements of existing tactics.
@@ -48,7 +46,9 @@ on http://www.labri.fr/~casteran/CoqArt.
 
   The sources of Coq V8.0 beta, including its integrated development
 environment, are available from http://coq.inria.fr/ and
-ftp://ftp.inria.fr/INRIA/LogiCal/coq/V8.0beta/.
+ftp://ftp.inria.fr/INRIA/LogiCal/coq/V8.0beta/. The translation
+package coq-8.0beta-translator.tar.gz is available separately at
+the same location.
 
   Please refer to the accompanying document CHANGES or the location
 ftp://ftp.inria.fr/INRIA/LogiCal/coq/V8.0beta/doc/Changes.html for a
@@ -57,11 +57,6 @@ full list of changes including sources of incompatibilities.
   The (at the time partial) documentation of Coq V8.0 is available in
 postscript, pdf and html format.
 
-# Si on a le temps...
-  Notice that you can browse the new standard library at
-http://coq.inria.fr/library-eng.html (these pages have been generated
-by coqdoc).
-
   Users are kindly invited to report bugs at http://coq.inria.fr/bin/coq-bugs
 and to mail Coq-Club@pauillac.inria.fr for general questions or remarks.
 Note that you can now choose your personal options at