The Coq documentation
                           =====================

The Coq documentation includes

- A Reference Manual
- A Tutorial
- A document presenting the Coq standard library
- A list of questions/answers in the FAQ style

The sources of the documents are mainly made of LaTeX code from which
user-readable PostScript or PDF files, or a user-browsable bunch of
html files are generated.

Prerequisite
------------

To produce all the documents, the following tools are needed:

  - latex (latex2e)
  - pdflatex
  - dvips
  - bibtex
  - makeindex
  - fig2dev (transfig)
  - convert (ImageMagick)
  - hevea
  - hacha


Under Debian based operating systems (Debian, Ubuntu, ...) a
working set of packages for compiling the documentation for Coq is:

  texlive texlive-latex-extra texlive-math-extra texlive-fonts-extra
  texlive-humanities texlive-pictures latex-xcolor hevea transfig
  imagemagick


Compilation
-----------

To produce all documentation about Coq, just run:

   make doc


Alternatively, you can use some specific targets:

   make doc-ps
   	to produce all PostScript documents

   make doc-pdf
        to produce all PDF documents

   make doc-html
        to produce all html documents

   make refman
        to produce all formats of the reference manual

   make tutorial
        to produce all formats of the tutorial

   make rectutorial
        to produce all formats of the tutorial on recursive types

   make faq
        to produce all formats of the FAQ

   make stdlib
        to produce all formats of the Coq standard library


Installation
------------

To install all produced documents, do:

  make DOCDIR=/some/directory/for/documentation install-doc

DOCDIR defauts to /usr/share/doc/coq