Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Pretty conversion of Coq to HTML?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Pretty conversion of Coq to HTML?


Chronological Thread 
  • From: François Pottier <francois.pottier AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Pretty conversion of Coq to HTML?
  • Date: Wed, 12 Jul 2017 15:02:57 +0200


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/



Archive powered by MHonArc 2.6.18.

Top of Page