The Coq mailing list

[Lélio Brun <lelio.brun AT inria.fr>]

Hello, 

the nicest pretty-printing I've seen so far was here: 
https://homes.cs.washington.edu/~jrw12/dep-destruct.html
I don't think it uses proviola, which indeed seems to be unmaintained. 
Maybe you could ask directly the author of the post: 
jrw12 AT cs.washington.edu

Lélio Brun

----- Mail original -----
> De: "Gaetan Gilbert" 
> <gaetan.gilbert AT ens-lyon.fr>
> À: 
> coq-club AT inria.fr
> Envoyé: Mercredi 12 Juillet 2017 15:07:07
> Objet: Re: [Coq-Club] Pretty conversion of Coq to HTML?
> 
> If you mean this
> http://hott.github.io/HoTT/proviola-html/HoTT.Spaces.Nat.html it's
> proviola https://arxiv.org/abs/1005.2672
> 
> I think its site is dead though.
> 
> Gaëtan Gilbert
> 
> On 12/07/2017 15:02, François Pottier 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/
> 
>