The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

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.