The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 08/06/2012 08:08 AM, Jason Gross wrote:
> Is there a variant of [change _ with _ in *] that does not fail if 
> [change _ with _ in H] fails for some particular hypothesis, but 
> succeeds for all the other ones?

Perhaps this fits the bill?


Ltac change_everywhere X Y :=
  repeat match goal with
        | [ H : context[X] |- _ ] =>
          match type of H with
            | context[Y] => fail 1
            | _ => change X with Y in H
      end
  end;
  try change X with Y.