The Coq mailing list

[Gregory Malecha <gmalecha AT eecs.harvard.edu>]

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/