coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] extraction of natural language from proofs

From: CHA Reeseo <reeseo AT formal.korea.ac.kr>
To: coq-club <coq-club AT pauillac.inria.fr>
Subject: Re: [Coq-Club] extraction of natural language from proofs
Date: Sat, 6 Jun 2009 04:33:02 +0900
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:content-type :content-transfer-encoding; b=T0GaEgeuw3kApO5qnthErLvqPxCaSBddzMq9i/HBPU1nFhnfqYDJJNrVfsCTAlaWa9 DIatwmeeSsAiu5IFwcchO1ZRIgc4+OytA2W1zq50D3/ifjxQsZDeMQR0dT/2cYu2r+Ui Rjvj9rWvKhzaabJHX79FhGS+ZN4xjz5SoSbEw=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

2009/6/5 Ryan Rusich
<rusichr AT cs.ucr.edu>:
> Dear All, Can anyone point me in the direction of the documentation for
> extracting natural language from proofs using Coq? I read that it was
> included in Coq from version 6.2 on, but have run into some difficulty
> identifying the name of the command, and the location documentation
> pertaining to it on the Coq website.

Do you happen to want coqdoc?

http://coq.inria.fr/coq/distrib/current/refman/Reference-Manual018.html#toc93

--
CHA Reeseo
http://www.reeseo.net/

[Coq-Club] extraction of natural language from proofs, Ryan Rusich
- Re: [Coq-Club] extraction of natural language from proofs, Guilhem Moulin
  - Re: [Coq-Club] extraction of natural language from proofs, Lukasz Stafiniak
  - Re: [Coq-Club] extraction of natural language from proofs, Ryan Rusich
- Re: [Coq-Club] extraction of natural language from proofs, CHA Reeseo
- Re: [Coq-Club] extraction of natural language from proofs, Yves Bertot
  - Re: [Coq-Club] extraction of natural language from proofs, Ryan Rusich