The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

It is our pleasure to announce a beta release of Coq version 8.1.
The main features of this new version are

- efficient evaluation

  - new auxiliary algorithm for checking the convertibility of types,
    specially dedicated to fast type-checking of reflexion-based proofs,
    and more generally to intensive computation

- inductive types

  - support for recursively non uniform parameters
  - support for some form of sort-polymorphism that leads to merge
    prod and prodT, list and listT, etc.

- improved/extended tactics

  - new implementation of setoid rewrite (contributed by C. Sacerdoti Coen)
  - many other new tactic features (see attached file CHANGES)

- libraries
 
  - finite sets and finite maps (by J.-C. Filliâtre and P. Letouzey)
  - strings (by L. Théry)
  - significative extensions of the library on lists
  - some other extensions (see attached file CHANGES)
  - rational numbers (by P. Letouzey) [rational are defined as a quotient 
    over Z/Z+* -- an alternative library based on the canonical Stern-Brocot
    representation is available in the user contributions]

- experimental features

  - new command to generate proof obligations from definitions of
    programs required to meet their specification (see chapter 19 in
    the reference manual)
  - mechanism to communicate with external tool, such as computer
    algebra systems or theorem provers able to generate proofs (see the
    end of chapter 9 in the reference manual)

and many other features mentioned in the attached CHANGES file.

A large amount of known bugs have been fixed (see coq-bugs at
http://coq.inria.fr for details).

Coq version 8.1 hopefully comes with only a few incompatibilities (see
http://coq.inria.fr/V8.1beta/COMPATIBILITY). 

The documentation will be progressively completed in the next
weeks at http://coq.inria.fr/V8.1beta/refman.

A few precompiled packages are available from http://coq.inria.fr/V8.1beta. ;
Extra precompiled packages will be added soon.

Coq version 8.1 is based on the new Coq version 8.0 syntax. Users
migrating from Coq version 7.x and older must first translate their
developments from the old syntax using the translator provided with
Coq version 8.0.

Bug reports may be submitted at http://pauillac.inria.fr/bin/coq-bugs
and general questions or remarks can be sent to 
Coq-Club AT pauillac.inria.fr.
 
The Coq development team