The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Can do something like (untested):

Ltac do_change x A B tac :=
let H := fresh in
pose x as H;
change A with B in x;
let x' := eval unfold H in H;
clear H;
tac x'.

?

-Jason

On Mar 22, 2013 2:18 PM, "Gregory Malecha" <gmalecha AT eecs.harvard.edu> wrote:

Hello --

Is there a way in Ltac to run [change] on a term? For example, I'd like to do:

let x := eval change A with B in x in ....

in order to change all of the uses of A with B.

Ideally I would be able to do this without a [match ... with context [ A ] => ... end].

Thanks.

--
gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/