Version preliminaire pour la V8

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

1 files changed, 41 insertions, 15 deletions

diff --git a/ANNONCE b/ANNONCE
index 7463db95a..af6d7c7a2 100644
--- a/ANNONCE
+++ b/ANNONCE
@@ -1,27 +1,53 @@
-The Coq development team is pleased to announce the release of Coq
-version 7.4. 
 
-  This version provides several novelties, including a new system of
-parametric modules and interfaces, and support for the Why
-(http://why.lri.fr) and Krakatoa (http://www.lri.fr/~marche/krakatoa)
-systems. However, this version is still experimental and does not
-fully support the functionalities of the previous version 7.3.1
-(especially ast-based grammar extensions are off).
+  The Coq development team is pleased to announce Coq version 8.0, a new
+major evolution of the Coq system.
+
+  First, the logical system of Coq version 8.0 has been simplified by
+removing the impredicativity of the sort Set. This allows to benefit
+of the principle of description in formalisations of classical
+mathematics without leading to logical inconsistencies. Impredicativity
+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,
+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
+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.
+
+  Thirdly, the standard library has been revised and simplified. There
+is now only one equality "=" and one existential quantification valid
+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 brings also improved tactics (especially refined
+conversion and induction tactics).
 
   Please refer to the accompanying document CHANGES or the location
-ftp://ftp.inria.fr/INRIA/LogiCal/coq/V7.4/doc/Changes.html for a full list of
-changes including sources of incompatibilities.
+ftp://ftp.inria.fr/INRIA/LogiCal/coq/V8.0/doc/Changes.html for a full
+list of changes including sources of incompatibilities.
 
-  Coq V7.4 is available in several formats from http://coq.inria.fr/
-and ftp://ftp.inria.fr/INRIA/coq/V7.4/
+  Coq V8.0 is available in several formats from http://coq.inria.fr/
+and ftp://ftp.inria.fr/INRIA/coq/V8.0/
 
   The documentation is available in postscript, pdf and html format.
 
-  Notice that you can browse the standard library at 
-http://coq.inria.fr/library-eng.html (these pages have been generated 
+  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
+p  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