MAJ

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

1 files changed, 11 insertions, 7 deletions

diff --git a/ANNONCE b/ANNONCE
index af6d7c7a2..4598d3071 100644
--- a/ANNONCE
+++ b/ANNONCE
@@ -10,12 +10,12 @@ remains available as an option for experimented users still wishing to
 require this feature.
 
   Secondly, Coq version 8.0 comes with a completely new syntax of
-terms, and a revised uniformised syntax for tactics and
-commands. Besides a better uniformity and a lightening of the syntax,
+terms, and a revised more uniform syntax for tactics and
+commands. Besides a better uniformity and a simplification of the syntax,
 the purpose is to allow the use of high-level comforts, such as
 implicit types in quantification and notations for standard
 arithmetical notions (e.g. +,*,<,<=) without conflicts with the rest
-of syntax. A new notion of "interpretation scopes" allows also to
+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
@@ -27,13 +27,17 @@ on all types. The type "R" is now in Set and the library on Z has been
 re-organised. The basic notions from the initial state now have
 implicit arguments.
 
-  Coq version 8.0 comes with an automatic translator from old to new
-syntax. Follow the instructions in document ??? from the distribution
-to update your developments from old to new syntax.
+  Coq version 8.0 comes with a 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.
 
   Coq version 8.0 brings also improved tactics (especially refined
 conversion and induction tactics).
 
+  Last but not the least, Coq version 8.0 comes with a new integrated
+gtk-based user interface in the style of ProofGeneral.
+
   Please refer to the accompanying document CHANGES or the location
 ftp://ftp.inria.fr/INRIA/LogiCal/coq/V8.0/doc/Changes.html for a full
 list of changes including sources of incompatibilities.
@@ -47,7 +51,7 @@ and ftp://ftp.inria.fr/INRIA/coq/V8.0/
 http://coq.inria.fr/library-eng.html (these pages have been generated
 by coqdoc).
 
-p  Users are kindly invited to report bugs at http://coq.inria.fr/bin/coq-bugs
+  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
 http://pauillac.inria.fr/mailman/listinfo/coq-club and consult the