mirror of
https://github.com/msgpack/msgpack-c.git
synced 2025-03-20 05:27:56 +01:00
5 lines
153 B
Coq
5 lines
153 B
Coq
Ltac rewrite_for x :=
|
|
match goal with
|
|
| [ H : x = _ |- _ ] => rewrite H in *; clear H
|
|
| [ H : _ = x |- _ ] => rewrite <- H in *; clear H
|
|
end. |