coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] extraction of natural language from proofs

From: Ryan Rusich <rusichr AT cs.ucr.edu>
To: coq-club <coq-club AT pauillac.inria.fr>
Subject: [Coq-Club] extraction of natural language from proofs
Date: Fri, 5 Jun 2009 07:57:31 -0700
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:from:date:x-google-sender-auth:message-id :subject:to:content-type; b=hrueOpMqlx+wWkLpg0edq98gTYX2eMJ8lTfpElcA69yUn0c0tIfaPfyx1yBh2hC0+u S79cOlIGlubRDZeEfLwPK3NpKJ+38iK88roIxXP2uYPkw+rPeUWFt7/R/t0nXAct/hii RE5eRuv8YMnFCnJn7u6HYbBWkQHyQTrIajlXA=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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.�

Thank you,
Ryan

[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