From mboxrd@z Thu Jan 1 00:00:00 1970 From: Alan Schmitt Subject: Re: adding rudimentary support for Coq code blocks Date: Fri, 07 Feb 2014 16:40:22 +0100 Message-ID: References: <87d2j0c4f3.fsf@gmail.com> Mime-Version: 1.0 Content-Type: text/plain Return-path: Received: from eggs.gnu.org ([2001:4830:134:3::10]:50757) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1WBnbx-0003eB-1N for emacs-orgmode@gnu.org; Fri, 07 Feb 2014 10:45:06 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1WBnbr-0003M5-41 for emacs-orgmode@gnu.org; Fri, 07 Feb 2014 10:45:00 -0500 Received: from mail2-relais-roc.national.inria.fr ([192.134.164.83]:61725) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1WBnbq-0003M0-UQ for emacs-orgmode@gnu.org; Fri, 07 Feb 2014 10:44:55 -0500 In-Reply-To: <87d2j0c4f3.fsf@gmail.com> (Eric Schulte's message of "Thu, 06 Feb 2014 14:32:12 -0700") List-Id: "General discussions about Org-mode." List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: emacs-orgmode-bounces+geo-emacs-orgmode=m.gmane.org@gnu.org Sender: emacs-orgmode-bounces+geo-emacs-orgmode=m.gmane.org@gnu.org To: Eric Schulte Cc: Org Mode Mailing List Eric Schulte 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