The Coq mailing list

[Stéphane Glondu <steph AT glondu.net>]

Le 15/08/2010 18:15, Michael a écrit :
> I tried to automatize it with Ltac like this:
> Ltac myTac:=
> match goal with
>   |- func ?x (?y) =>
>   replace (func x y) with (func x y - 1 + 1)
> end.

This will match only goals with "func" as head symbol. If you want to
match "func" in any context, you should use:

Ltac myTac:=
match goal with
  |- context [ func ?x (?y) ] =>
  replace (func x y) with (func x y - 1 + 1)
end.

It will then match "x * func a (b+c) <= y * z", for example.


Cheers,

-- 
Stéphane