*** empty log message ***

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

1 files changed, 25 insertions, 4 deletions

diff --git a/ANNONCE b/ANNONCE
index 94aa5f5a0e..27bf4ac0b4 100644
--- a/ANNONCE
+++ b/ANNONCE
@@ -6,8 +6,12 @@ version 7.3. This release offers the following novelties or improvements:
 - 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).
-- New tactic "Rename x into y" for renaming hypotheses.
-- New tactics "Pose x:=u" and "Pose u" to add definitions to local context.
+- 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
@@ -15,8 +19,17 @@ version 7.3. This release offers the following novelties or improvements:
   the Zsgn function, more induction principles (Wf_Z.v and
   tail of Zcomplements.v) and one more general Euclid theorem.
 
-  Inversion has been improved and Intuition simplified but not in a fully
-compatible way.
+  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).
@@ -37,12 +50,20 @@ following versions
 
   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 (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
 changes including sources of incompatibilities.
 
   Users are kindly invited to report bugs to coq-bugs@pauillac.inria.fr
 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