The Coq mailing list

[Matthieu Sozeau <Matthieu.Sozeau AT lri.fr>]

Le 29 janv. 09 à 23:43, Woon Ming a écrit :

> Hi all,

Hi,

> In my Ltac,  I would like to detect the occurrence of a particular  
> keyword in the conclusion and apply the appropriate hypothesis.
> ( e.g.
> My conclusion consists of “a * b = keyword * b”.
> And my ltac is something like this:
>
> Ltac simplify :=
> match goal with
> | [id:(_=?key) |- (_ = key * b)] => rewrite id.
> end.
> )
> In the example given, it is workable only because I specified the  
> operator (*). However, in the case where I don’t specify any  
> operator (e.g. (_ =key_)), this is completely not workable. Is there  
> any way I can perform regex matching in a generalized manner (e.g.  
> without specifying the operator)?

Yes, using the [context [ pat ]] pattern construction.
It is documented in the reference manual.

-- Matthieu