Mise a jour V7

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

1 files changed, 26 insertions, 14 deletions

diff --git a/ANNONCE b/ANNONCE
index 7e33b5dcce..a8b4eeef26 100644
--- a/ANNONCE
+++ b/ANNONCE
@@ -1,7 +1,6 @@
 
   The LogiCal team (ex-Coq team) is releasing a new version of Coq
-(V7.0beta). This new version is still under development and is
-provided for users willing to experiment the new features which are:
+(V7.0). The new features are:
 
   - a primitive let-in construct
   - qualified names (such as Logic.f_equal)
@@ -10,13 +9,16 @@ provided for users willing to experiment the new features which are:
     (by David Delahaye)
   - an improved Search facilities using patterns (by Yves Bertot)
   - a "natural" syntax for real numbers (by Micaela Mayero)
+  - a new implementation of the extraction from Coq proofs to Ocaml programs
+    (by J.-C. Filliātre and P. Letouzey)
+  - an improved reduction strategy for lazy evaluation (by B. Barras)
   - various bug fixes
   - a command to export theories to XML to be used with Helm's publishing
     and rendering tools (see http://www.cs.unibo.it/helm) (by Claudio
     Sacerdoti Coen)
 
-  Extraction and the Realizer/Program tactics are not available in Coq
-V7.0beta.
+  The Realizer/Program tactics are not available in Coq V7.0.
+  The Correctness command can be used instead.
 
   The internals of Coq have changed a lot and this justifies the new
 major version number 7 though the differences are small for end-users
@@ -24,20 +26,30 @@ The internals of Coq will continue to change significantly in the next
 months and we recommend tactic developers to take contact with us for
 adapting their code.
 
-  Coq V7.0beta is a minimal version. User contributions and full
-documentation are not updated. No binary package is provided for
-Windows or MacOS.
-
-  Coq V7.0beta is available as a source package from http://coq.inria.fr
+  Coq V7.0 is available in several formats from http://coq.inria.fr 
 and ftp://ftp.inria.fr/INRIA/coq/V7. 
+  We currently provide the following versions
+
+	package for sources
+	rpm package for sources
+	rpm package for linux
+	binary package for Sun-Solaris
+	binary version for Windows
+
+	No binary package is provided for MacOS.
+
+  The documentation has been updated and is available in postscript, 
+pdf and html format.
+
+  User's contributions are not yet available
 
   Please refer to the accompanying document Changes.dvi for a full
 list of changes including sources of incompatibilities (very few).
 
-  Users are kindly invited to provide feedback on the new features by mailing
-to coq@pauillac.inria.fr for bug reports or to Coq-Club@pauillac.inria.fr for
-general questions or remarks (moderated).
-
+  Users are kindly invited to provide feedback on the new features by
+mailing to coq-bugs@pauillac.inria.fr for bug reports or to
+Coq-Club@pauillac.inria.fr for general questions or remarks
+(moderated).
 
-  Jean-Christophe Filliātre and Hugo Herbelin
+	The Coq development team