The Coq mailing list

[Yucheng Zhang <yczhang89 AT gmail.com>]

On Jun 21, 2013, at 6:47 PM, Math Prover 
<mathprover AT gmail.com>
 wrote:
> Lastly, if the "right" way to do this to use some external tool which
> looks at a *.v file and generates a separate file with the
> declarations, I'm okay with that too.


I am using the 'coqdoc' tool partially for this purpose. It can be run with
options --gallina and --light, either of which can suppress proofs in the
output. The generated HTMLs have cross references, which are convenient for
browsing.

The CompCert C compiler uses its own tool 'coq2html', generating nice looking
HTMLs powered by JavaScripts, where proofs are hidden by default, and can be
expanded upon clicking.