The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Luminous Fennell wrote:
> Over the holidays, I wrote some Haskell code to export Coq definitions
> to LaTeX or ASCII documents.[...]
>
> My questions is, if it would be worth it to put a little bit more effort
> in this (i.e. making a real project out of this). Is there already such
> a tool? And if not would anybody else be interested or find this useful?
>    

Have you looked at coqdoc, which is included in the standard Coq 
distribution?  It has been used successfully to typeset several books.  
(It only covers LaTeX and HTML, not ASCII.)