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.
Information regarding Project Releases and Project Resources. Note that the information here is a quote from Freecode.com page, and the downloads themselves may not be hosted on OSDN.
Cette version apporte des classes de style Haskell-type, différentes évolutions des bibliothèques de l'arithmétique, et de nombreuses autres améliorations et extensions concernant le système de modules, la tactique, la syntaxe, etc
Tags:
Major feature enhancements
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.
L'argument profondeur de recherche de l'auto peut être paramétrée dans la langue LTAC. L'entrée constr_may_eval a été ajouté pour les extensions tactique. Un couple de lemmes de ZArith ont été renommés. Cela concerne les noms contenant O (la lettre), qui est remplacée par 0 (le nombre).
Tags:
Minor feature enhancements
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).
GPL-incompatible fichiers QPL pour CoqIde sont maintenant sous la licence GPL. Pretty-impression des coercitions à Funclass ont été corrigés et améliorés.
Tags:
Minor bugfixes
GPL-incompatible QPL files for CoqIde are now under the GPL. Pretty-printing of coercions to Funclass were fixed and improved.
Il s'agit d'une nouvelle évolution majeure du système Coq. Il dispose d'un système logique plus extensible en raison de la suppression de la Imprédicativité du genre Set, une syntaxe complètement nouvelle, un traducteur automatique de l'ancienne à la nouvelle syntaxe, une nouvelle notion de "champs d'interprétation", une version révisée et simplifiée bibliothèque standard , une tactique de nouveaux automatismes pour les déclarations du premier ordre, et une interface GTK intégrée nouvelle interface utilisateur.
Tags:
Major feature enhancements
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.
