The Coq development team is pleased to release version 7.1 of Coq.
This release is a major update on version 6.3.1 and a bug-fixes update
on version 7.0.

  The main features of Coq versions 7.0 and 7.1 on version 6.3.1 are

  - a primitive let-in construct
  - qualified names
  - library structuration
  - a high-level tactic language
  - improved search facilities
  - export of theories to XML for publishing and rendering purposes
  - a deep restructuration of the code (safer, simpler and more efficient)
  - 

  Compared to version 7.0, the new version provides with

  - port of user contributions (including new libraries for
    constructive complex analysis, floating-point numbers, P-automaton
    and graph theory, and formalizations of the ABR algorithm, CTL and
    TCTL temporal logic, the Railroad Crossing Problem, a subset of the
    C language, imperative Bresenham line drawing algorithm, imperative
    Marché's minimal edition distance algorithm, Buchberger's algorithm,
    RSA cryptographic algorithm, Stalmarck tautology checker algorithm,
    the Fundamental Theorem of Algebra and ZFC set theory).
  - new tactics NewDestruct, NewInduction and Assert intended to
    improve the behaviour of previous Elim and Induction, Case and
    Destruct, and Cut tactics
  - known-bugs fixes
  - excessive memory use mainly fixed

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

  Coq V7.1 is available in several formats from http://coq.inria.fr
and ftp://ftp.inria.fr/INRIA/coq/V7.1. 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
  binary version for MacOS X (without specific GUI)

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

  Please refer to the accompanying document CHANGES 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 (moderated).

  The Coq development team (in LogiCal team)