12.6 Coq and HTML
As for LATEX, it is also possible to pretty print Coq listing with
HTML. The document looks like the LATEX one, with links added when
possible : links to other Coq modules in Require commands, and
links to identifiers defined in other modules (when they are found in a
path given with -I options).
In regular mode, the command
% coq2html file.v
produces an HTML document file.html.
See the man page of coq2html for more details and options.