.TH COQDOC 1
.
.SH NAME
coqdoc \- documentation tool for the Coq proof assistant
.
.
.SH SYNOPSIS
.B coqdoc
[
options
]
.I files
.
.
.SH DESCRIPTION
.
.B 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).
.
.
.SH OPTIONS
.
.SS Overall options
.
.TP
.B \-h
Help.
Will give you the complete list of options accepted by
.BR coqdoc .
.TP
.B \-\-html
Select a HTML output.
.TP
.B \-\-latex
Select a LaTeX output.
.TP
.B \-\-dvi
Select a DVI output.
.TP
.B \-\-ps
Select a PostScript output.
.TP
.B \-\-texmacs
Select a TeXmacs output.
.TP
.B \-\-stdout
Redirect the output to stdout
.TP
.BI \-o \ file, \-\-output \ file
Redirect the output into the file
.I file.
.TP
.BI \-d \ dir, \ \-\-directory \ dir
Output files into directory
.I dir
instead of current directory (option
.B \-d
does not change the filename specified with option
.BR \-o ,
if any).
.TP
.BR \-s , \ \-\-short
Do not insert titles for the files.
The default behavior is to insert a title like ``Library Foo'' for each
file.
.TP
.BI \-t \ string, \ \-\-title \ string
Set the document title.
.TP
.B \-\-body\-only
Suppress the header and trailer of the final document.
Thus, you can insert the resulting document into a larger one.
.TP
.BI \-p \ string, \ \-\-preamble \ string
Insert some material in the LaTeX preamble, right before
\\begin{document} (meaningless with \-html).
.TP
.BI \-\-vernac\-file \ file, \ \-\-tex\-file \ file
Considers the file
.I file
respectively as a .v (or .g) file or a .tex file.
.TP
.BI \-\-files\-from \ file
Read file names to process in file
.I file
as if they were given on the command line.
Useful for program sources split in several directories.
.TP
.BR \-q , \ \-\-quiet
Be quiet.
Do not print anything except errors.
.TP
.BR \-h , \ \-\-help
Give a short summary of the options and exit.
.TP
.BR \-v , \ \-\-version
Print the version and exit.
.
.SS Index options
.
Default behavior is to build an index, for the HTML output only, into
index.html.
.
.TP
.B \-\-no\-index
Do not output the index.
.TP
.B \-\-multi\-index
Generate one page for each category and each letter in the index,
together with a top page index.html.
.
.SS Table of contents option
.
.TP
.BR \-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.
.
.SS Hyperlinks options
.
.TP
.BI \-\-glob\-from \ file
Make references using Coq globalizations from file file.
(Such globalizations are obtained with Coq option
.BR \-dump\-glob ).
.
.TP
.B \-\-no\-externals
Do not insert links to the Coq standard library.
.
.TP
.BI \-\-external \ url\ libroot
Set base URL for the external library whose root prefix is
.I libroot.
.
.TP
.BI \-\-coqlib_url \ url
Set base URL for the Coq standard library (default is
http://coq.inria.fr/library/).
.
.TP
.BI \-\-coqlib \ dir
Set the base path where the Coq files are installed, especially style
files coqdoc.sty and coqdoc.css.
.
.TP
.BI \-R \ dir\ coqdir
Map physical directory dir to Coq logical directory coqdir (similarly
to Coq option
.BR \-R ).
.B Note:
option
.B \-R
only has effect on the files following it on the command
line, so you will probably need to put this option first.
.
.SS Contents options
.
.TP
.BR \-g , \ \-\-gallina
Do not print proofs.
.
.TP
.BR \-l , \ \-\-light
Light mode. Suppress proofs (as with
.BR \-g )
and the following commands:
.RS
.IP \(bu 3
[Recursive] Tactic Definition
.IP \(bu
Hint / Hints
.IP \(bu
Require
.IP \(bu
Transparent / Opaque
.IP \(bu
Implicit Argument / Implicits
.IP \(bu
Section / Variable / Hypothesis / End
.PP
The behavior of options
.B \-g
and
.B \-l
can be locally overridden using the
(*\ begin show\ *) .\|.\|. (*\ end show\ *) environment (see above).
.RE
.
.SS Language options
.
Default behavior is to assume ASCII 7 bits input files.
.
.TP
.BR \-latin1 , \ \-\-latin1
Select ISO-8859-1 input files.
It is equivalent to
.BR "\-\-inputenc\ latin1 \-\-charset\ iso\-8859\-1" .
.
.TP
.BR \-utf8 , \ \-\-utf8
Select UTF-8 (Unicode) input files.
It is equivalent to
.BR "\-\-inputenc\ utf8 \-\-charset\ utf\-8" .
LaTeX UTF-8 support can be found at
http://www.ctan.org/tex\-archive/macros/latex/contrib/supported/unicode/.
.
.TP
.BI \-\-inputenc \ string
Give a LaTeX input encoding, as an option to LaTeX package inputenc.
.
.TP
.BI \-\-charset \ string
Specify the HTML character set, to be inserted in the HTML header.
.
.
.SH SEE ALSO
.
.I
The Rocq Prover Reference Manual.
.PP
The Rocq Prover website: https://rocq-prover.org