Quick Navigator

Search Site

Unix VPS
A - Starter
B - Basic
C - Preferred
D - Commercial
MPS - Dedicated
Previous VPSs
* Sign Up! *

Contact Us
Online Help
Domain Status
Man Pages

Virtual Servers

Topology Map

Server Agreement
Year 2038

USA Flag



Man Pages

Manual Reference Pages  -  COQDOC (1)


coqdoc - A documentation tool for the Coq proof assistant


     Overall options
     Index options
     Table of contents option
     Hyperlinks options
     Contents options
     Language options
See Also


coqdoc [ options ] files


coqdoc is a documentation tool for the Coq proof assistant. It creates LaTeX or HTML documents from a set of Coq files. See the Coq reference manual for documentation (url below).


    Overall options

-h Help. Will give you the complete list of options accepted by coqdoc.
--html Select a HTML output.
--latex Select a LATEX output.
--dvi Select a DVI output.
--ps Select a PostScript output.
  Select a TeXmacs output.
  Redirect the output to stdout
-o file,--output file
  Redirect the output into the file file.
-d dir, --directory dir
  Output files into directory dir instead of current directory (option -d does not change the filename specified with option -o, if any).
-s, --short Do not insert titles for the files. The default behavior is to insert a title like ‘‘Library Foo’’ for each file.
-t string, --title string
  Set the document title.
  Suppress the header and trailer of the final document. Thus, you can insert the resulting document into a larger one.
-p string, --preamble string
  Insert some material in the LATEX preamble, right before \begin{document} (meaningless with -html).
--vernac-file file, --tex-file file
  Considers the file ‘file’ respectively as a .v (or .g) file or a .tex file.
--files-from file
  Read file names to process in file ‘file’ as if they were given on the command line. Useful for program sources split in several directories.
-q, --quiet Be quiet. Do not print anything except errors.
-h, --help Give a short summary of the options and exit.
-v, --version Print the version and exit.

    Index options

Default behavior is to build an index, for the HTML output only, into index.html.

  Do not output the index.
  Generate one page for each category and each letter in the index, together with a top page index.html.

    Table of contents option

-toc, --table-of-contents
  Insert a table of contents. For a LATEX output, it inserts a \tableofcontents at the beginning of the document. For a HTML output, it builds a table of contents into toc.html.

    Hyperlinks options

--glob-from file
  Make references using Coq globalizations from file file. (Such globalizations are obtained with Coq option -dump-glob).

  Do not insert links to the Coq standard library.

--external url libroot
  Set base URL for the external library whose root prefix is libroot.

--coqlib url
  Set base URL for the Coq standard library (default is

--coqlib_path dir
  Set the base path where the Coq files are installed, especially style files coqdoc.sty and coqdoc.css.

-R dir coqdir
  Map physical directory dir to Coq logical directory coqdir (similarly to Coq option -R). Note: option -R only has effect on the files following it on the command line, so you will probably need to put this option first.

    Contents options

-g, --gallina
  Do not print proofs.

-l, --light Light mode. Suppress proofs (as with -g) and the following commands:

* [Recursive] Tactic Definition
* Hint / Hints
* Require
* Transparent / Opaque
* Implicit Argument / Implicits
* Section / Variable / Hypothesis / End

The behavior of options -g and -l can be locally overridden using the (* begin show *) ... (* end show *) environment (see above).

    Language options

Default behavior is to assume ASCII 7 bits input files.

-latin1, --latin1
  Select ISO-8859-1 input files. It is equivalent to --inputenc latin1 --charset iso-8859-1.

-utf8, --utf8
  Select UTF-8 (Unicode) input files. It is equivalent to --inputenc utf8 --charset utf-8. LATEX UTF-8 support can be found at

--inputenc string
  Give a LATEX input encoding, as an option to LATEX package inputenc.

--charset string
  Specify the HTML character set, to be inserted in the HTML header.


The Coq Reference Manual from

Search for    or go to Top of page |  Section 1 |  Main Index

--> COQDOC (1) April, 2006

Powered by GSP Visit the GSP FreeBSD Man Page Interface.
Output converted with manServer 1.07.