The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

This is untested, but I suspect it will work:

Ltac pattern2 term var :=

    let term' := pattern var in term in

    change term with term'.

-Jason

On Thu, Apr 24, 2014 at 7:48 AM, Cedric Auger <sedrikov AT gmail.com> wrote:

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\...