The Coq mailing list

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

Dear Coq-Club members,

After a long maturation, Coq 8.2 is now out! As already partially
mentioned on this list, Coq 8.2 brings Haskell-style type classes,
various evolutions of the arithmetic libraries (machine-word-based
arithmetic, abstract arithmetic, the Micromega solvers framework), a
stand-alone checker for cross-certification of proofs and many other
various improvements and extensions regarding the module system,
tactics, syntax, ... (see http://coq.inria.fr/V8.2/description.html
for details and http://coq.inria.fr/V8.2/CHANGES for a full log of
changes).

The major source of incompatibilities comes from the new
implementation of setoid rewrite, and marginally, from the support of
constant unfolding in apply. A secondary source of incompatibilities
stems out of some bug fixes and of changes in specific libraries. See
http://coq.inria.fr/V8.2/COMPATIBILITY for details and migration
recommendations.

We named the package coq-8.2-1 as the preliminary package coq-8.2
previously available for a few days on the Coq web site had an
installation problem. A binary package for windows is available for
download from the Coq web site (http://coq.inria.fr) and one for Mac
OS X will be released in a few days.

Thanks to Objective Caml 3.11 new native code dynamic loading feature, we
are happy to announce a new support for plugins to Coq. Especially, two
Coq extensions are already known to be compatible with the plugins system:
- G. Gonthier's Ssreflect tactics and libraries
- A. Miquel's extraction for classical logic in Prop

(of course, this requires a version of Coq and of the extensions
 compiled with ocaml 3.11)

Note the following new user contributions submitted since 8.1 was
released:

- A logical Toolkit for Multimodal Categorial Grammars (H. Anoun, P. Castéran)
- Tutorial on Reflecting in Coq the generation of Hoare proof obligations (S. 
Boulmé)
- A survey of semantics styles (Y. Bertot)
- Tarski's geometry (J. Narboux)
- Hypermaps, Genus Theorem and Euler Formula (J.-F. Dufourd)
- Ruler and compass geometry axiomatization (J. Duprat)
- Projective Plane Geometry (N. Magaud, J. Narboux, P. Schreck)
- JProver: A theorem prover for first-order intuitionistic logic (H. 
Guan-Shieng)
- Tortoise and the hare algorithm (J.-C. Filliâtre)
- A formalisation of Pure Type Systems (B. Barras)
- Higman's lemma on an unrestricted alphabet (W. Delobel)
- Efficient Reduction of Large Integers by Small Moduli (L. Rutten)
- Finite orbit-stabilizer theorem (R. Kam)
- Fundamental theorems of arithmetic (S. Briais)
- Problem 11262 of The American Mathematical Monthly (M. Niqui, T. Hurkens)
- Real numbers as coinductive ternary streams (M. Niqui)
- Coalgebras, bisimulation and lambda-coiteration (M. Niqui)
- CompCert, a Certified C Compiler (X. Leroy et al., release 1.3)
- An extended version of the CoLoR library
- An extended version of the Constructive Coq Repository at Nijmegen (CoRN)

The Coq development team