The Coq mailing list

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

Coq version 8.1 is finally enriched of two new major changes : new
implantations of the simplification tactics in rings and fields and an
experimental declarative mathematical proof language. This justifies
to keep version 8.1 in testing mode for an extra period and we
packaged to this aim a version called 8.1 gamma.

The updated list of the main features of Coq 8.1 over 8.0 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 (by B. Grégoire)

- inductive types

  - support for recursively non uniform parameters (by C. Paulin)
  - support for some form of sort-polymorphism that leads to merge
    prod and prodT, list and listT, etc. (by H. Herbelin)

- improved/extended tactics

  - new implementation of setoid rewrite (by C. Sacerdoti Coen)
  - improved implementation of simplification in rings (by B. Grégoire, 
    A. Mahboubi and B. Barras)
  - improved implementation of simplification in fields (by L. Théry 
    and B. Barras)
  - 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)
  - extensions of the library on lists (by P. Letouzey and J.-M. Notin)
  - 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]
  - a few other evolutions (see attached file CHANGES)

- experimental features

  - new command Function to generate fixpoints with arbitrary well-
    foundedness termination evidence and associated "functional"
    induction scheme, fixpoint equation, and support for inversion
    (by P. Courtieu and J. Forest and by Y. Bertot)
  - new command to generate proof obligations from definitions of
    programs required to meet their specification (see chapter 19 in
    the reference manual) (by M. Sozeau)
  - 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)
  - new declarative mathematical proof language (by P. Corbineau)

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 gamma is available in several formats at address
http://coq.inria.fr/V8.1gamma. The documentation is located at
http://coq.inria.fr/V8.1gamma/refman.

The main sources of incompatibilites of Coq version 8.1 gamma come
from the new implementations of the tactics setoid_rewrite, ring and
field. See http://coq.inria.fr/V8.1gamma/COMPATIBILITY for details
and smooth migration recommendations.

Coq version 8.1 gamma 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://coq.inria.fr/bin/coq-bugs
and general questions or remarks can be sent to 
Coq-Club AT pauillac.inria.fr.
See http://pauillac.inria.fr/mailman/listinfo/coq-club for
your personal options. A mail archive is available at
http://pauillac.inria.fr/pipermail/coq-club.
 
New contributions have been submitted. See http://coq.inria.fr for details.
 
The Coq development team