---
name: "coq2html"
section: "1"
platform: "linux"
package: "coq"
version: "6.3.1-2"
release: "Debian 2.2 (Potato)"
platforms: ["linux"]
url: "https://new.carta.tech/coq2html"
---

# coq2html(1)

formats Coq files into HTML documents

## 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)](/coqdep/1.md) 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 **coq@pauillac.inria.fr**