coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] CoqdocJS: foldable proofs and better Unicode support for Coqdoc

From: Clément Pit--Claudel <clement.pit AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] CoqdocJS: foldable proofs and better Unicode support for Coqdoc
Date: Sun, 15 May 2016 09:26:08 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=clement.pit AT gmail.com; spf=SoftFail smtp.mailfrom=clement.pit AT gmail.com; spf=None smtp.helo=postmaster AT mout.kundenserver.de
Ironport-phdr: 9a23:nzL3rRezBVx687VtQcnz8UlzlGMj4u6mDksu8pMizoh2WeGdxc6+YR7h7PlgxGXEQZ/co6odzbGG4ua6BSdeu96oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDjvcePKFsSzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IAu3GePEzSqUdBzA7OUg04tfqvF/NV1ih/HwZB04SEx9FBRTy1BDmG9LatiLnuud5kH2ROcDzQLYoHyyj849kTRbpjGEMMDtvozKfsdB5kK8O+EHpnBd42YOBOIw=

Wonderful job! Hopefully this gets merged into CoqDoc proper soon :)

On 2016-05-13 15:15, Tobias Tebbi 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
> .
>

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] CoqdocJS: foldable proofs and better Unicode support for Coqdoc, Tobias Tebbi, 05/13/2016
- Re: [Coq-Club] CoqdocJS: foldable proofs and better Unicode support for Coqdoc, Gabriel Scherer, 05/15/2016
  - Re: [Coq-Club] CoqdocJS: foldable proofs and better Unicode support for Coqdoc, Bas Spitters, 05/15/2016
- Re: [Coq-Club] CoqdocJS: foldable proofs and better Unicode support for Coqdoc, Clément Pit--Claudel, 05/15/2016