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.