Skip to Content.
Sympa Menu

coq-club - [Coq-Club] extraction of natural language from proofs

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] extraction of natural language from proofs


chronological Thread 
  • 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



Archive powered by MhonArc 2.6.16.

Top of Page