We are pleased to release a *beta* version of Coq 8.2 which brings
Haskell-style type classes, various evolutions of the arithmetic
libraries, and many other various improvements and extensions
regarding the module system, tactics, syntax, etc.

The support for Haskell-style type classes has been contributed by
M. Sozeau and is documented in chapter 18 of the reference manual.

The evolutions of the arithmetic libraries cover the following points:
- use of native arithmetic in the bytecode-based fast evaluator of Coq
  (A. Spiwack),
- new library on efficient 31-bits integer and word-based unbounded 
  integers (L. Théry, B. Grégoire, A. Spiwack, P. Letouzey),
- new library on axiomatic natural, cyclic and unbounded integer
  numbers (E. Makarov),
- new framework "micromega" for solving systems of inequalities in Z, Q, R,
  possibly relying on external tool for non linear systems (F. Besson).

The module system has been extended with the include feature, sharing
of common submodules, functorial signature application and on-demand
parameter inlining (E. Soubiran).

At the level of tactics, Coq 8.2 offers a more efficient implementation
of setoid rewrite, new support for constant unfolding in apply, new
dependent induction, induction/destruct with "in" clause and "e"
variants, support for iteration and "at" clause in rewrite, new
variants of introduction patterns, support for implicit contents and
coercions in the "with" clauses, use of type informations in
unification (P. Letouzey, M. Sozeau, S. Glondu, E. Makarov,
H. Herbelin).

Coq 8.2 also offers miscellaneous syntax extensions and improved
features: destructing let, better type inference, inference of
matching return clause, detection of impossible clause in dependent
pattern-matching, detection of decreasing argument in fixpoints,
improved Program and Function features, new ways to work with implicit
arguments, and various other auxiliary features (M. Sozeau,
P. Letouzey, H. Herbelin). It also provides automatic generation of
decidable equality (V. Siles).

Finally, Coq comes with a new stand-alone checker for
cross-certification of vo-files (B. Barras).

For all other changes, see the attached file CHANGES.

The major sources of incompatibilities comes from the support of
constant unfolding in apply and from the new implementation of setoid
rewrite. A secondary source comes from some bug fixes and from changes
in specific libraries. See http://coq.inria.fr/COMPATIBILITY for
details and smooth migration recommendations. We are interested in
feedback on the upgrading problems that may be encountered.

The documentation is available at http://coq.inria.fr/V8.2beta/doc/refman.

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.

Here follows a list of user contributions submitted since the release
of Coq 8.1 (see the Coq web site for download):

The Coq development team