Overalloptions-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
-ofile,--outputfile
Redirect the output into the file file.-ddir,--directorydir
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.
-tstring,--titlestring
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.
-pstring,--preamblestring
Insert some material in the LaTeX preamble, right before \begin{document} (meaningless with
-html).
--vernac-filefile,--tex-filefile
Considers the file file respectively as a .v (or .g) file or a .tex file.
--files-fromfile
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.
Indexoptions
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.
Tableofcontentsoption-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.
Hyperlinksoptions--glob-fromfile
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.
--externalurllibroot
Set base URL for the external library whose root prefix is libroot.--coqlib_urlurl
Set base URL for the Coq standard library (default is http://coq.inria.fr/library/).
--coqlibdir
Set the base path where the Coq files are installed, especially style files coqdoc.sty and
coqdoc.css.
-Rdircoqdir
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.
Contentsoptions-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).
Languageoptions
Default behavior is to assume ASCII 7 bits input files.
-latin1, --latin1
Select ISO-8859-1 input files. It is equivalent to --inputenclatin1--charsetiso-8859-1.
-utf8, --utf8
Select UTF-8 (Unicode) input files. It is equivalent to --inputencutf8--charsetutf-8. LaTeX
UTF-8 support can be found at
http://www.ctan.org/tex-archive/macros/latex/contrib/supported/unicode/.
--inputencstring
Give a LaTeX input encoding, as an option to LaTeX package inputenc.
--charsetstring
Specify the HTML character set, to be inserted in the HTML header.
Install Now
PNG Icons
