The Coq tool is a proof assistant which is able to handle calculus assertions, to check proofs of these assertions mechanically, and to extract a certified program from the constructive proof of its formal specification.
|Operating Systems||Mac OS X Windows POSIX Linux|
Release Notes: Various bugs were fixed.
Release Notes: This release 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.
Release Notes: The search depth argument of auto can be parameterised in the Ltac language. The constr_may_eval entry was added for tactic extensions. A couple of lemmas of ZArith were renamed. This concerns names containing O (the letter), which is replaced by 0 (the number).
Release Notes: GPL-incompatible QPL files for CoqIde are now under the GPL. Pretty-printing of coercions to Funclass were fixed and improved.
Release Notes: This is a new major evolution of the Coq system. It features a more extensible logical system due to the removal of the impredicativity of the sort Set, a completely new syntax, an automatic translator from the old to the new syntax, a new notion of "interpretation scopes", a revised and simplified standard library, a new automation tactic for first-order statements, and a new integrated GTK-based user interface.