The Coq mailing list

["Woon Ming" <woon_ming AT comp.nus.edu.sg>]

Hi all,

 

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)?  

 

Best Regards,

Woon Ming

HP: 92981768