The Coq mailing list

[Olivier Desmettre <desmettr AT pauillac.inria.fr>]

  The Coq development team is pleased to announce the release of Coq
version 7.3. This release offers the following novelties or
improvements:

- 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.

  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)

  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 AT pauillac.inria.fr
and to mail 
Coq-Club AT 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