Coq version 8.1 is finally out. It fixes many bugs of Coq version
8.1gamma and can be considered "stable". Compared to 8.1gamma, the
ring and field tactics have also been extended to deal with the power
function and to rewrite monomials on the fly (see documentation).

Compared to Coq 8.0, the main changes are the following:

- 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)

See the attached CHANGES file for the full list of new features.

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

The documentation is available from http://coq.inria.fr.

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.

For the list of known bugs or to submit a new one, see page Contacts
at http://coq.inria.fr. General questions or remarks can be sent to
Coq-Club@pauillac.inria.fr. See also http://coq.inria.fr.

The main changes in the Objective Caml interfaces of Coq are
documented in the file dev/doc/changes.txt of Coq source archive.

Here follows a list of user contributions submitted in the past two
years (see the Coq web site for download):

- CoLoR: a library on rewriting and termination (F. Blanqui, S. Hinderer,
  S. Coupet-Grimal, W. Delobel, A. Koprowski)
- Library for persistent union-find (J.-C. Filliâtre)
- Micromega: reflexive tactics for Presburger arithmetic and more (F. Besson)
- Up-to techniques for weak bisimulation (D. Pous)
- Higher-order syntax from modules over monads (A. Hirschowitz, M. Maggesi) 
- Bisimulation for the spi-calculus (S. Briais)
- Modelization of random programs (C. Paulin)
- An approach of proof by reflexion for first-order logic (P. Corbineau)
- Another approach of proof by reflexion for first-order logic (D. Hendriks)
- Intuitionistic propositional checker (K. Weich)
- Chou-Gao-Zhang area method for deciding affine geometry (J. Narboux)
- Proof of the Fairisle 4x4 Switch Element (S. Coupet-Grimal, L. Jakubiec)
- Kildall's data-flow analysis (S. Coupet-Grimal, W. Delobel)
- Diophantus' 20th Problem and Fermat's last theorem for n=4 (D. Delahaye, 
  M. Mayero)
- Karatsuba multiplication on binary numbers (R. O'Connor)
- Case study on square matrices (J.-C. Filliâtre)
- Divide-and-conquer for binary tree diameter computation (J.-C. Filliâtre)
- Certified Sudoku solver (L. Théry)
- Ordinals (Cantor, Veblen), hydra battle, Goodstein sequences (P. Castéran, 
  E. Contejean)
- The Godel-Rosser 1st incompleteness theorem (R. O'Connor)
- Embedding intuitionistic ZF set theory in Coq + intuit. choice (A. Miquel)
- Category theory in set theory (C. Simpson)
- Tait-style normalizability for simply-typed lambda-calculus (P. Letouzey, 
  H. Schwichtenberg)

The Coq development team