diff options
Diffstat (limited to 'src/Util/Tactics/DestructTrivial.v')
| -rw-r--r-- | src/Util/Tactics/DestructTrivial.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/Util/Tactics/DestructTrivial.v b/src/Util/Tactics/DestructTrivial.v new file mode 100644 index 000000000..716e953fb --- /dev/null +++ b/src/Util/Tactics/DestructTrivial.v @@ -0,0 +1,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. |