The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

I don’t know if that would help you, but you should be able to do:

change (x^2) with ((fun x => x^2) x).

With Ltac and tactic Notations, there may be a way to implement your "pattern2" with that.

2014-04-23 12:30 GMT+02:00 Kate and James Candy <jacinabox AT hotmail.com>:

Lately I've been wishing for a smarter pattern tactic, that can be made to do its work in a subterm of the goal. For example, if the goal is (P (x ^ 2 * exp x)), I could do pattern2 (x ^ 2) x and get the goal (P ((fun x => x ^ 2) x * exp x)).

--jacinabox

--
.../Sedrikov\...