Package coq-8.3pl3-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 coq tools, together with documentation for the standard library; the files to build custom tactics in Ocaml are available in `coq-dev'; the reference manual and some other documentation is available in the `coq-doc' package; a graphical user environment is contained in the `coqide' package.