MAJ

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

1 files changed, 10 insertions, 7 deletions

diff --git a/ANNONCE b/ANNONCE
index 4482ee2754..81d2671400 100644
--- a/ANNONCE
+++ b/ANNONCE
@@ -1,7 +1,7 @@
 
-  The LogiCal team (ex-Coq team) is releasing a new version of Coq.
-Its name is V7.0beta. This new version is provided for users willing
-to experiment the new features which are:
+  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:
 
   - a primitive let-in construct
   - qualified names (such as Logic.f_equal)
@@ -19,9 +19,9 @@ V7.0beta.
 
   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
-(e.g. most error messages are located). 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.
+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
@@ -33,7 +33,10 @@ and ftp://ftp.inria.fr/INRIA/coq/V7.
   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).
 
-  Jean-Christophe Filliātre and Hugo Herbelin
 
+  Jean-Christophe Filliātre and Hugo Herbelin