The Coq mailing list

[François Pottier <francois.pottier AT inria.fr>]

Hello,

I believe I have seen somewhere (during an academic presentation, 
probably) a
tool that converts Coq files to HTML files, with the feature that 
pointing the
mouse cursor anywhere in the middle of a rendered proof script causes the
current proof state (hypotheses and goal) to be displayed. I can't remember
how it is called, and I can't find it, though. Any help would be welcome.
Thanks,

--
François Pottier
francois.pottier AT inria.fr
http://gallium.inria.fr/~fpottier/