blob: 716e953fb2d00d99cbb06ed898f6f58f3b13b490 (
plain)
1
2
3
4
5
6
|
Ltac destruct_trivial_step :=
match goal with
| [ H : unit |- _ ] => clear H || destruct H
| [ H : True |- _ ] => clear H || destruct H
end.
Ltac destruct_trivial := repeat destruct_trivial_step.
|