coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adamc AT csail.mit.edu>
- To: Jason Gross <jasongross9 AT gmail.com>
- Cc: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] non-failing version of [change _ with _ in *]?
- Date: Mon, 06 Aug 2012 08:40:06 -0400
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.
- [Coq-Club] non-failing version of [change _ with _ in *]?, Jason Gross, 08/06/2012
- Re: [Coq-Club] non-failing version of [change _ with _ in *]?, Adam Chlipala, 08/06/2012
Archive powered by MHonArc 2.6.18.