The LogiCal team (ex-Coq team) is releasing a new version of Coq
(V7.0). The new features are:

  - a primitive let-in construct
  - qualified names (such as Logic.f_equal)
  - a more high-level tactic language based on a small functional core with
    recursors and elaborated matching operators for terms and proof contexts
    (by David Delahaye)
  - an improved Search facilities using patterns (by Yves Bertot)
  - a "natural" syntax for real numbers (by Micaela Mayero)
  - a new implementation of the extraction from Coq proofs to Ocaml programs
    (by J.-C. Filliātre and P. Letouzey)
  - an improved reduction strategy for lazy evaluation (by B. Barras)
  - various bug fixes
  - a command to export theories to XML to be used with Helm's publishing
    and rendering tools (see http://www.cs.unibo.it/helm) (by Claudio
    Sacerdoti Coen)

  The Realizer/Program tactics are not available in Coq V7.0.
  The Correctness command can be used instead.

  The internals of Coq have changed a lot and this justifies the new
major version number 7 though the differences are small for end-users
The internals of Coq will continue to change significantly in the next
months and we recommend tactic developers to take contact with us for
adapting their code.

  Coq V7.0 is available in several formats from http://coq.inria.fr 
and ftp://ftp.inria.fr/INRIA/coq/V7. 
  We currently provide the following versions

	package for sources
	rpm package for sources
	rpm package for linux
	binary package for Sun-Solaris
	binary version for Windows

	No binary package is provided for MacOS.

  The documentation has been updated and is available in postscript, 
pdf and html format.

  User's contributions are not yet available

  Please refer to the accompanying document Changes.dvi for a full
list of changes including sources of incompatibilities (very few).

  Users are kindly invited to provide feedback on the new features by
mailing to coq-bugs@pauillac.inria.fr for bug reports or to
Coq-Club@pauillac.inria.fr for general questions or remarks
(moderated).

	The Coq development team