The Coq mailing list

[Alan Schmitt <alan.schmitt AT polytechnique.org>]

On 2016-06-16 18:30, James Wilcox 
<wilcoxjay AT gmail.com>
 writes:

> It's pretty embarrassing to show this dirty hack in public. Surely there is 
> a
> better way! 

I don't know if this is better, and it clearly is ugly without a nice
CSS and syntax highlighting (both are easy to set up), but I use
org-mode to document and execute Coq developments. Here is an example
input file http://alan.petitepomme.net/tips/test_coq_exec.org and the
resulting output http://alan.petitepomme.net/tips/test_coq_exec.html.
The glue code to do it is at
http://alan.petitepomme.net/tips/executing_coq.html

To document Coq code from outside the development (if you don't want to
have too much prose in your code), you can use this approach
http://alan.petitepomme.net/tips/documenting_coq.html

Best,

Alan

-- 
OpenPGP Key ID : 040D0A3B4ED2E5C7
Monthly Athmospheric CO₂, Mauna Loa Obs. 2015-05: 403.94, 2016-05: 407.70

Attachment: signature.asc
Description: PGP signature