The LogiCal team (ex-Coq team) is releasing a new version of Coq
(V7.0beta). This new version is still under development and is
provided for users willing to experiment the new features which 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)
  - 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)

  Extraction and the Realizer/Program tactics are not available in Coq
V7.0beta.

  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.0beta is a minimal version. User contributions and full
documentation are not updated. No binary package is provided for
Windows or MacOS.

  Coq V7.0beta is available as a source package from http://coq.inria.fr
and ftp://ftp.inria.fr/INRIA/coq/V7. 

  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@pauillac.inria.fr for bug reports or to Coq-Club@pauillac.inria.fr for
general questions or remarks (moderated).


  Jean-Christophe Filliātre and Hugo Herbelin