[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.
Alan