List of additionnal documentation

This manual contains not all the documentation the user may need about Coq. Various informations can be found in the following documents:

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.
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.