coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adamc AT csail.mit.edu>
- To: robert <robdockins AT fastmail.fm>
- Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Ltac question/challenge: working with open terms
- Date: Sun, 15 Sep 2013 15:42:50 -0400
On 09/15/2013 03:25 PM, robert wrote:
Have you read Section 15.5 of CPDT <http://adam.chlipala.net/cpdt/>? I haven't read all of the code you included, but the prose makes it sound like that section shows how to do what you're looking for. |
- [Coq-Club] Ltac question/challenge: working with open terms, robert, 09/15/2013
- Re: [Coq-Club] Ltac question/challenge: working with open terms, Adam Chlipala, 09/15/2013
- [Coq-Club] Ltac question/challenge: working with open terms, Jason Gross, 09/15/2013
- Re: [Coq-Club] Ltac question/challenge: working with open terms, robert, 09/16/2013
- Re: [Coq-Club] Ltac question/challenge: working with open terms, Adam Chlipala, 09/17/2013
- Re: [Coq-Club] Ltac question/challenge: working with open terms, Jason Gross, 09/18/2013
- Re: [Coq-Club] Ltac question/challenge: working with open terms, Adam Chlipala, 09/17/2013
- Re: [Coq-Club] Ltac question/challenge: working with open terms, Adam Chlipala, 09/15/2013
Archive powered by MHonArc 2.6.18.