Coq 8.2
Coq 8.2 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 tools 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). The mathematical proof language is documented in chapter 11 of the reference manual (P. Corbineau).
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 CHANGES file.
As far as we could judge, the major sources of incompatibilities come from the new implementation of setoid rewrite and, marginally, from the support of constant unfolding in apply. A secondary source comes from some bug fixes and from changes in specific libraries. See the COMPATIBILITY file for details and smooth migration recommendations. We are interested in feedback on the upgrading problems that may be encountered.
The documentation is available online.
You can submit the bugs you encounter on the bug tracker. General questions or remarks can be sent to coq-club@inria.fr.
A few changes in the Objective Caml interfaces of Coq are documented in the file dev/doc/changes.txt of Coq source archive.
| Sources | ||
| coq-8.2pl3.tar.gz | 3.5 MB | |
| Binaries | ||
 Windows
|
coq-8.2pl2-win-1.exe | 138 MB |
 MacOS
|
coq-8.2pl3-macosx.dmg | 29 MB |
| coqide-8.2pl3-macosx.dmg (Coq bundled with CoqIDE interface) | 49 MB | |
| These binary packages should work for Mac OS 10.5, 10.6 and 10.7. If you wish to compile your own version of Coq, you may follow these instructions to build a MacOS package using MacPorts | ||
| Documentation | ||
| Tutorial.pdf | 0.2 MB | |
| Reference-Manual.pdf | 2 MB | |