This is the latest stable release of the Coq system (see the detailed description and the full list of changes).

Sources
	coq-8.2pl1.tar.gz	3.5 MB
Binaries
Windows	coq-8.2pl1-win-1.exe	138 MB
MacOS	coq-8.2-intel.dmg	90 MB
	Warning: This binary package contains Coq 8.2pl0 and was built for Mac OS 10.5. If you wish to use a newer version of Coq, or install it under Mac OS 10.6, you may follow these instructions to build a MacOS package using MacPorts
Documentation
	Tutorial.pdf	0.2 MB
	Reference-Manual.pdf	2 MB

The last patch level for Coq 8.1 series is 8.1pl5. It has been released on june 2009.

Sources
	coq-8.1pl5-1.tar.gz	3 MB
Binaries
Windows	coq-8.1pl5-1-win.exe	111 MB
Documentation
	Tutorial.pdf	0.2 MB
	Reference-Manual.pdf	2 MB

The development version of Coq is browsable and downloadable from our Subversion repository using command: svn checkout svn://scm.gforge.inria.fr/svn/coq/trunk

Most of the previous version of Coq are available here for the most recent ones and here for the older ones.

When compiled with Objective Caml 3.11 (which is the case of the Windows and MacOS packages we release), Coq supports dynamic loading of extensions. Two extensions are known to work as plugins:

• The small scale reflection package (ssreflect) contains the robust and compact tactic language and basic libraries that served, among other applications, as support for the full formalization of the 4 color theorem in Coq.
• The classical extraction module provides extraction of programs from classical proofs in Prop.

Note: Objective Caml ≥ 3.11.1 is required for building plugins on MacOS 10.5.