The Coq Proof Assistant

Coq version 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 (see the more detailed description and the summary of changes).

We cared for backward compatibility but some specific features may require a few adaptations for upgrading. This is specially the case of (more efficient) setoid rewriting and of the library of functional sets and maps. If you encounter a migration problem not mentioned in the list of known incompatibilities, this can be considered as a bug.

Coq 8.2 is currently released in beta test. We thank beta-tester in advance for feedback on the new version. There is a list of known bugs.