diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-25 12:42:18 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-25 13:38:06 -0400 |
| commit | 01a6557cd14bab453f09ec4448682f05bdb607f6 (patch) | |
| tree | 17b9a109ea4955dc5660da30d8a7a02f1993544e /src/Util/Tactics | |
| parent | 2647f37bb4c814061190fdc8e62993acd27cfdb4 (diff) | |
Add destruct_head'_sum
Diffstat (limited to 'src/Util/Tactics')
| -rw-r--r-- | src/Util/Tactics/DestructHead.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/Util/Tactics/DestructHead.v b/src/Util/Tactics/DestructHead.v index fa7693e5e..fe56278e4 100644 --- a/src/Util/Tactics/DestructHead.v +++ b/src/Util/Tactics/DestructHead.v @@ -58,3 +58,8 @@ Ltac destruct_one_head'_or := match goal with H : or _ _ |- _ => destruct H end. Ltac destruct_one_head_or := destruct_one_head'_or; simpl in *. Ltac destruct_head'_or := repeat destruct_one_head'_or. Ltac destruct_head_or := repeat destruct_one_head_or. + +Ltac destruct_one_head'_sum := match goal with H : sum _ _ |- _ => destruct H end. +Ltac destruct_one_head_sum := destruct_one_head'_sum; simpl in *. +Ltac destruct_head'_sum := repeat destruct_one_head'_sum. +Ltac destruct_head_sum := repeat destruct_one_head_sum. |