coqdoc - A documentation tool for the Coq proof assistant
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).
- -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.
- --texmacs
- Select a TeXmacs output.
- --stdout
- 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.
- --body-only
- 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.
Default behavior is to build an index, for the HTML output only,
into index.html.
- --no-index
- Do not output the index.
- --multi-index
- Generate one page for each category and each letter in the index, together
with a top page index.html.
- -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.
- --glob-from
file
- Make references using Coq globalizations from file file. (Such
globalizations are obtained with Coq option -dump-glob).
- --no-externals
- 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
http://coq.inria.fr/library/).
- --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.
- -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).
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
http://www.ctan.org/tex-archive/macros/latex/contrib/supported/unicode/.
- --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 http://coq.inria.fr/