The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

This is indeed nice. It seems to have some overlap in goals with
http://mws.cs.ru.nl/proviola/


On Sun, May 15, 2016 at 2:38 PM, Gabriel Scherer
<gabriel.scherer AT gmail.com>
 wrote:
> This is very nice, thanks!
>
> Do you think that it would eventually make sense to integrate this
> into upstream coqdoc?
> In my experience, people do not necessarily take the time to inform
> themselves about the various coqdoc-improvements option laying around;
> they want to get a reasonable HTML rendering real quick, and are
> likely to use exactly what is most easy to run from their existing
> development -- which is likely to be the coqdoc-related target of
> coq_makefile's output. To reach a large number of user, being enable
> "by default" is thus fairly important.
>
> On Fri, May 13, 2016 at 3:15 PM, Tobias Tebbi 
> <ttebbi AT ps.uni-saarland.de>
>  wrote:
>> Hi,
>>
>> I wrote some Javascript to improve the output of Coqdoc by adding foldable
>> proofs and extensible replacement of ASCII with Unicode such that 
>> copy-paste
>> still produces ASCII.
>> You can have a look at the result here:
>> https://www.ps.uni-saarland.de/autosubst/doc/Ssr.POPLmark.html
>>
>> This is really easy to integrate into any Coq development, see here:
>> https://www.ps.uni-saarland.de/~ttebbi/coqdocjs/
>>
>> Best,
>> Tobias