Premier jet annonce 8.1

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

1 files changed, 19 insertions, 77 deletions

diff --git a/ANNONCE b/ANNONCE
index 1f507a3f1..5e634f2cb 100644
--- a/ANNONCE
+++ b/ANNONCE
@@ -1,85 +1,27 @@
+The main features of Coq version 8.1 are
 
-  Coq version 8.0 is a major evolution of the Coq system. The final
-version of is now coming out.
+- the implementation of an alternative algorithm for checking the
+  convertibility of types, specially dedicated to fast type-checking
+  of reflexion-based proofs, and more generally to intensive
+  computation
 
-Coq version 8.0 features
-------------------------
+- richer inductive types
 
-  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.
+  - support for recursively non uniform parameters
+  - support for a strong form of sort-polymorphism
 
-  Secondly, Coq version 8.0 comes with a completely new syntax of
-terms, and a slightly revised 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 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).
+- improved tactics
 
-  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.
+  - new implementation of setoid rewrite (contributed by C. Sacerdoti Coen)
+  - new implementation of ring (contributed by B. Grégoire and A. Mahboubi)
+  - and several other new tactic features
 
-  Coq version 8.0 comes with a smart and robust comment-preserving
-automatic translator from old to new syntax. A translation package
-with a documentation of the new syntax accompanies the distribution.
+- new libraries
+ 
+  - finite sets and finite maps (by J.-C. Filliâtre and P. Letouzey)
+  - strings (by L. Théry)
+  - significative extensions of the library on lists
+  - a few other extensions
 
-  Coq version 8.0 brings also a new automation tactic for first-order
-statements and various improvements of existing tactics.
-
-  Last but not the least, Coq version 8.0 comes with CoqIde, a new
-integrated gtk-based user interface in the style of ProofGeneral.
-
-New book on Coq
----------------
-
-  For the first time, a comprehensive textbook on the art of Coq,
-accompanies the distribution of Coq. We are extremely thankful to the
-authors, Yves Bertot and Pierre Casteran, for this essential
-contribution to the development of Coq. This 470-pages book comes with
-about 200 exercises and their solution in Coq. Details are on
-http://www.labri.fr/~casteran/CoqArt.
-
-Changes wrt Coq version 8.0 beta
---------------------------------
-
-  The main change wrt to Coq 8.0 beta is a different semantics for the
-if-then-else construction, which may lead to the need of rerunning the
-translator, or to modify a few lines by hand. The other modifications
-mainly consist in extensions or upgrading (a few tactics and commands,
-XML exportation of theories and proof scripts, coqdoc compatibility)
-and bug fixes. See file Changes.html on Coq web site for details.
-
-Downloading and documentation
------------------------------
-
-  The sources of Coq V8.0, including its integrated development
-environment, are available from http://coq.inria.fr/ and
-ftp://ftp.inria.fr/INRIA/LogiCal/coq/V8.0/. The translation package
-coq-8.0-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.0/doc/Changes.html for a
-full list of changes including sources of incompatibilities.
-
-  The documentation of Coq V8.0 is available in postscript, pdf and
-html format.
-
-  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 
-mails archive at http://pauillac.inria.fr/pipermail/coq-club.
-
-
-  The Coq development team
+- improved module system