mirror of
https://github.com/msgpack/msgpack-python.git
synced 2026-02-13 19:04:16 +00: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.
|