[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [O] adding rudimentary support for Coq code blocks

From: Alan Schmitt
Subject: Re: [O] adding rudimentary support for Coq code blocks
Date: Fri, 07 Feb 2014 16:40:22 +0100
User-agent: Gnus/5.13 (Gnus v5.13) Emacs/24.3 (darwin)

Eric Schulte <address@hidden> writes:

> See the attached example file.  This is very rudimentary, only
> supporting session evaluation and without support for smart translation
> between Org-mode and Coq data structures.

Very nice, thanks a lot!

I use org mode with Coq, but only to document Coq developments. See
http://jscert.org/dvpt.html for instance. By the way, I recently
converted two persons to org mode because of its abilities to easily
extract source code to pretty typesetting, both in HTML and LaTeX.


reply via email to

[Prev in Thread] Current Thread [Next in Thread]