Package coqide-8.0pl3-3

Developed in the LogiCal project (http://logical.inria.fr), the Coq tool is a formal proof management system: a proof done with Coq is mechanically checked by the machine. In particular, Coq allows one: * to define functions and predicates * to state mathematical theorems and software specifications * to develop interactively formal proofs of these theorems * to check these proofs by a small certification "kernel". Coq is based on a logical framework called "Calculus of Inductive Constructions" extended by a modular development system for theories. Coq also includes * a mecanism for automatically generating certified programs * proofs of the specifications of these programs * a documentation tool (coqdoc) * dependecy and makefile generation tools for Coq * a preprocessor for TeX files that include Coq commands (coq-tex) This package provides a graphical user interface (GTK+2) for Coq.