Coq 8.3
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 | |
dmg packages, use the Coq bug tracker.