Version V7.4

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

1 files changed, 11 insertions, 48 deletions

diff --git a/ANNONCE b/ANNONCE
index 27bf4ac0b..7829e98d8 100644
--- a/ANNONCE
+++ b/ANNONCE
@@ -1,52 +1,15 @@
   The Coq development team is pleased to announce the release of Coq
-version 7.3. This release offers the following novelties or improvements:
+version 7.4. 
 
-- New option -dump-glob to coqtop to dump globalizations (to be used by the 
-  new documentation tool coqdoc; see http://www.lri.fr/~filliatr/coqdoc).
-- Elimination to Set/Type from empty propositions and to Type from
-  "singleton" propositions now allowed (as a consequence eqT_rec and
-  False_rec are now automatically available).
-- Tactics:
-  - New "Rename x into y" for renaming hypotheses.
-  - New "Pose x:=u" and "Pose u" to add definitions to local context.
-  - Tactic Definition's without arguments now allowed in Coq states.
-  - Inversion has been improved and Intuition simplified but not in a 
-    fully compatible way.
-- Record's now accept anonymous fields "_" (no projection is built then)
-- Haskell extraction now operational.
-- Extensions of [ZArith]: Zcomplements.v, Zpower.v and Zlogarithms.v
-  have been moved from contrib/omega to ZArith. They now include
-  the Zsgn function, more induction principles (Wf_Z.v and
-  tail of Zcomplements.v) and one more general Euclid theorem.
+This is not a major release, the main purpose this version is to offer novelties 
+(including the module system) required by the Why 
+(http://why.lri.fr) and Krakatoa (http://www.lri.fr/~marche/krakatoa) 
+systems. 
+See file CHANGES for a detailed list of changes, novelties, 
+bug-fixes and incompatibilities. 
 
-  We would also like to thank our users for their new contributions 
-(all compatible with Coq V7.3):
-  
-- CongruenceClosure: Congruence Closure Decision Procedure 
-  (Pierre Corbineau, ENS Cachan)
-- MapleMode: A Maple Mode for Coq 
-  (David Delahaye, Micaela Mayero, Chalmers University)
-- Presburger: A formalization of Presburger's algorithm 
-  (Laurent Thery, INRIA Sophia Antipolis)
-- ZChinese: A proof of the Chinese Lemma (based on ZArith) 
-  (Pierre Letouzey, LRI Orsay)
-
-  Most known bugs of version 7.2 are fixed (for the current status of
-reported bugs, see http://coq.inria.fr/bin/coq-bugs).
-
-  Pcoq user interface (http://www-sop.inria.fr/lemme/pcoq) is not
-ported to V7.3 yet.
-
-  Coq V7.3 is available in several formats from http://coq.inria.fr
-and ftp://ftp.inria.fr/INRIA/coq/V7.3. We currently provide the
-following versions
-
-  package for sources
-  rpm package for sources
-  rpm packages for linux
-  binary package for Sun-Solaris
-  binary version for Windows
-  binary version for MacOS X (Darwin)
+  Coq V7.4 is available in several formats from http://coq.inria.fr
+and ftp://ftp.inria.fr/INRIA/coq/V7.4.
 
   The documentation is available in postscript, pdf and html format.
 
@@ -55,10 +18,10 @@ http://coq.inria.fr/library-eng.html (this pages have been generated
 by coqdoc).
 
   Please refer to the accompanying document CHANGES or the location
-ftp://ftp.inria.fr/INRIA/coq/V7.3/doc/Changes.html for a full list of
+ftp://ftp.inria.fr/INRIA/coq/V7.4/doc/Changes.html for a full list of
 changes including sources of incompatibilities.
 
-  Users are kindly invited to report bugs to coq-bugs@pauillac.inria.fr
+  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