Man page - coqdoc(1)

Packages contains this manual

Package: coq
apt-get install coq

Manuals in package:

Documentations in package:

Manual

COQDOC

NAME
SYNOPSIS
DESCRIPTION
OPTIONS
Overall options
Index options
Table of contents option
Hyperlinks options
Contents options
Language options
SEE ALSO

NAME

coqdoc - documentation tool for the Coq proof assistant

SYNOPSIS

coqdoc [ options ] files

DESCRIPTION

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).

OPTIONS

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.

--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.

Index options

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.

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 ).

--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 url

Set base URL for the Coq standard library (default is http://coq.inria.fr/library/).

--coqlib 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 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.