coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Pretty conversion of Coq to HTML?
Date: Wed, 12 Jul 2017 09:06:24 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk0-f51.google.com
Ironport-phdr: 9a23:wLXEuxD4VGYLRwy96QL0UyQJP3N1i/DPJgcQr6AfoPdwSPT4rsbcNUDSrc9gkEXOFd2CrakV1KyO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fdbghMhjexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoINTA5/mHZhMJzkaxVvg6uqgdlzILIeoyYLuZycr/fcN4cWGFPXtxRVytEAo6kc4YAFOoBPedDr4n9uVQOrga1CBWqBOz1zD9Hm2L90Kog3Os6EQHG3RcgH9IQv3TXttn6LqESXvqzzKbV1znDbvJW2Svy6IXTfRAhpOuDXbN0ccbL1UYvEAbFg0yWpIf4MT2V0eENvHKa7+pmTe+gl2knqxt3ojexwscsjpPFiZwIxVDZ7Sl5wYA1Jce5SEFhe9KkHoFQuzmBOIt3XsMtWHxotzo5yrIYpZ63Zi8KyI4oxxPZdveJcJCI7wr9WOqNJTp0nnFodbKlixqs7EStxPfwW8mp3FtMsyFLiMPDtmoX2BzW8sWHSuVy/kOm2TuX0gDc8OBEIUQtmarFKJ4t3qc8lpQTvEjeBCP2l0L2jKiZdkUg5Oek8fjoYrLjppOENo90jB/xMrg2l8ChHeg1NhICUmub9OimyrHv4EP0TK9Kg/EriqXZtYrVJcUfpq63GQ9V1YMj5g6lADi90NQYnGIHLFJbdxKElYTmIVfOL+r+DfiimViskTZrx+zJPrD6DZXNK2LMkLblfbpn90Fczw8zwchF551IErEBPO7zWkjpudPECR85KhW4zPrjCNVgzYwTQnmPA6+cMKPKq1CE/OMvI++WZI8UojnxMfYl5+S9xUM+zFQaZOyi2YYdICSzGe0jKEGEa1LthM0AGCEEpFxtYvbtjQirWz5SfHa/XOoV4Dg9BMryBI3DR5utjb/H1SGyGJEQZ2FaBXiDFH7pc8OPXPJaO3HaGdNojjFRDevpcIQmzxz77AI=

Perhaps you saw this:

https://bitbucket.org/Carst/proviola-source

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Wed, Jul 12, 2017 at 9:02 AM, François Pottier <francois.pottier AT inria.fr> wrote:

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/

[Coq-Club] Pretty conversion of Coq to HTML?, François Pottier, 07/12/2017
- Re: [Coq-Club] Pretty conversion of Coq to HTML?, Abhishek Anand, 07/12/2017
- Re: [Coq-Club] Pretty conversion of Coq to HTML?, Gaetan Gilbert, 07/12/2017
  - Re: [Coq-Club] Pretty conversion of Coq to HTML?, Lélio Brun, 07/14/2017
    - Re: [Coq-Club] Pretty conversion of Coq to HTML?, Gabriel Scherer, 07/14/2017
      - Re: [Coq-Club] Pretty conversion of Coq to HTML?, Emilio Jesús Gallego Arias, 07/15/2017