NAME
coq2html - formats Coq files into HTML documents
SYNOPSIS
coq2html [ - ] [ -f ] [ -filter ] [ -stdout ] [ -nodefs ] [ -t n ] [ -I directory ] file ...
DESCRIPTION
coq2html formats Coq files into HTML documents. Keywords are pretty printed in bold face, comments in fixed typewriter font. Links to other modules and identifiers defined in other modules are inserted into the resulting document.
In regular mode, coq2html processes the input file(s), translating each Coq file foo.v into a HTML document foo.html.
When a proof of name "bar" is encountered , or a definition of an object of name "bar", then a label for "bar" is inserted at this place in the HTML document. Conversely, when an indentifier is found, say "gee", that belongs to the already known labels, then "gee" appears as a link to the corresponding label.
Notice that such links may refer to other files. Indeed, each time a command "Require foo" is encountered, then coq2html looks for the file foo.html and, if it exists, it reads all the labels contained in foo.html. It also adds a link to the file foo.html. A search path for HTML files may be given using the -I option (see below). It implies that you must construct the HTML files in the same order that for compiling the correspondig Coq files (i.e. if foo.v requires bar.v then bar.html must be made before foo.html). You may use coqdep(1) with the option "-suffix html" to produce the right dependencies.
OPTIONS
- -stdout
-
Prints the resulting document(s) on standard output.
- -, -f, -filter
-
Filter mode: reads the standard input and prints on the standard output.
- -nodefs
-
Do not insert links for definitions.
- -t n
-
Set the tabbing value to n.
- -I directory
-
Adds directory to the path of directories searched for HTML files.
NOTES
Nested comments are correctly handled.
BUGS
Please report any bug to [email protected]