This version comes with many improvements of existing features, especially regarding the tactics, the module system, extraction, the type classes, the program command, libraries, coqdoc. It also includes a new tactic (nsatz, standing for Hilbert's NullStellensatz, that extends ring to systems of polynomial equations) and a few new libraries (a certification of mergesort, a new library of finite sets with computational and logical contents separated). For a full log of changes, see the file CHANGES.

Coq 8.3 is not entirely upward compatible with 8.2. The major incompatibilities can be easily treated by using the new -compat 8.2 option or by setting/unsetting adequate options. See the file COMPATIBILITY for details and migration recommendations.

Sources
	coq-8.3pl5.tar.gz	3.7 MB
Binaries
Windows	coq-8.3pl5-win-0.exe (bundled with CoqIDE)	49 MB
MacOS	coq-8.3pl5.dmg	61 MB
	coqide-8.3pl5.dmg (Coq bundled with CoqIDE interface)	78 MB
	The packages require MacOS ≥ 10.5
Documentation
	Tutorial.pdf	0.2 MB
	Reference-Manual.pdf	1.5 MB

On Linux, BSD or MacOS package-based distributions, Coq is released by the corresponding maintainers. For reports on the Windows package and the MacOS dmg packages, use the Coq bug tracker.