Package coq-8.0pl3-1

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 to automatically generate 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 the core of the coq package; a graphical user environment is contained in the `coqide' package.