The Coq mailing list

[Bart De Vylder <bartdevylder AT gmail.com>]

On Wed, Jun 13, 2012 at 7:44 PM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

On 06/13/2012 01:16 PM, Bart De Vylder wrote:

If I use Hint Extern to match against the goal somehow, I don't see how i can refer to 'some' hypothesis in the context.
I read in the docs that Hint Extern can also be used to match against a hypothesis in the context, but I can't find an example of the syntax to use.

You don't use some special [Hint Extern] support for matching hypotheses.  Rather, to the right of the [=>], you write normal Ltac code for hypothesis matching.

Ok, got it, thx.

-- 
Bart De Vylder

+32(0)496/558065

bartdevylder AT gmail.com