coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Tobias Tebbi <ttebbi AT ps.uni-saarland.de>
To: coq-club AT inria.fr
Subject: [Coq-Club] CoqdocJS: foldable proofs and better Unicode support for Coqdoc
Date: Fri, 13 May 2016 21:15:43 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ttebbi AT ps.uni-saarland.de; spf=None smtp.mailfrom=ttebbi AT ps.uni-saarland.de; spf=None smtp.helo=postmaster AT triton.rz.uni-saarland.de
Ironport-phdr: 9a23:fM5ZqRFt3JYd/pB4WAYlxZ1GYnF86YWxBRYc798ds5kLTJ75osuwAkXT6L1XgUPTWs2DsrQf27uQ6fmrADZRqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh7H0ocSYOl8ZzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IZ4yhIP99FeAQTGl+cjN92Mq+vh7aCACL+3E0U2MMkxMODRKWwgv9W8LNtSH7v/E15CSQN8y+GawoVD6o7o9zU1n1jiZCLDcw6mXejMA2gK8N80HpnAB234OBONLdD/F5ZK6IIIsX

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

[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