The Coq development team is announcing the release version 7.2 of
Coq. This release fixes several bugs of version 7.1 and offers the following 
novelties or improvements

  - Coercions allowed in Cases patterns
  - Extended standard library
  - Extended tactic "Assert H := P" for forward reasoning
  - New tactic "ClearBody H" to clear the body of definitions in local context
  - New declaration "Canonical Structure id = t : I" to help resolution of
    implicits in developments using Record/Structure (contributed by A. Saïbi)

  Coq V7.2 is available in several formats from http://coq.inria.fr
and ftp://ftp.inria.fr/INRIA/coq/V7.2. 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.

  Please refer to the accompanying document CHANGES or the location
ftp://ftp.inria.fr/INRIA/coq/V7.2/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.

  The Coq development team