The LogiCal team (ex-Coq team) is releasing a new version of Coq.
Its name is V7.0beta. This new version 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 new tactic language based on a mini functional language with higher-
    level pattern-matching constructs on goals (by David Delahaye)
  - an improved Search facilities using patterns (by Yves Bertot)
  - a "natural" syntax for real numbers (by Micaëla Mayero)
  - various bug fixes
  - a command to export definitions, theorems and proofs 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
(e.g. most error messages are located). 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).


  Jean-Christophe Filliâtre and Hugo Herbelin