The Coq mailing list

[Luminous Fennell <mstrlu AT gmx.net>]

I sent this mail before, but it didn't seem to have come through... I'm
sorry if I'm mistaken and this is a double-post:

Hello list,

Over the holidays, I wrote some Haskell code to export Coq definitions
to LaTeX or ASCII documents. It's basically an xml parser and some
combinators to format/pretty-print the resulting AST. It's also not
documented and not very general (yet). I plan to use it for my master's
thesis (I'm a CS student into programming languages), in order to easily
print out and think about my newest type-system/semantics attempts,
without to type everything multiple times.

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?

I know about Ott, but it seems useful to me to export from Coq directly.

I know that HELM exists, but I couldn't even get past the front page
(http://helm.cs.unibo.it/library.html). I get ``cannot connect'' or 403
errors (Is there some good instructions anywhere how to use HELM?)

Best regards

Lu