Eric Schulte <schulte.e...@gmail.com> 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
