blob: 471f9c1a3a1c627a4353e5b68d157c89ee8e8540 (
plain)
1
2
3
4
5
6
|
Ltac clear_duplicates_step :=
match goal with
| [ H : ?T, H' : ?T |- _ ] => clear H'
| [ H := ?T, H' := ?T |- _ ] => clear H'
end.
Ltac clear_duplicates := repeat clear_duplicates_step.
|