List of additionnal documentation

Tutorial

A companion volume to this reference manual, the Coq Tutorial, is aimed at gently introducing new users to developing proofs in Coq without assuming prior knowledge of type theory. In a second step, the user can read also the tutorial on recursive types (document RecTutorial.ps).

Addendum

The fifth part (the Addendum) of the Reference Manual is distributed as a separate document. It contains more detailed documentation and examples about some specific aspects of the system that may interest only certain users. It shares the indexes, the page numbers and the bibliography with the Reference Manual. If you see in one of the indexes a page number that is outside the Reference Manual, it refers to the Addendum.

Installation

A text file INSTALL that comes with the sources explains how to install Coq. A file UNINSTALL explains how uninstall or move it.

Changes from Coq V6.1

This short note describes changes from Coq V6.1 to Coq V6.2. It is contained in the document Changes.ps.

The Coq standard library

A commented version of sources of the Coq standard library (including only the specifications, the proofs are removed) is given in the additional document Library.ps.