aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Tactics
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-12-12 22:07:25 -0500
committerGravatar Jason Gross <jgross@mit.edu>2017-12-12 22:07:25 -0500
commit6c9551617ea59f6a75e92505fdf197ca70c4d43f (patch)
treea31f0f833afa0ff1b934d4edf45aa301aa42ce49 /src/Util/Tactics
parent1536326649f2f9e47502332b7b0caaff7ebc153b (diff)
Add fast-path versions of [destruct_head] for unit,bool,True
Diffstat (limited to 'src/Util/Tactics')
-rw-r--r--src/Util/Tactics/DestructHead.v15
1 files changed, 15 insertions, 0 deletions
diff --git a/src/Util/Tactics/DestructHead.v b/src/Util/Tactics/DestructHead.v
index fe56278e4..94c1d601a 100644
--- a/src/Util/Tactics/DestructHead.v
+++ b/src/Util/Tactics/DestructHead.v
@@ -63,3 +63,18 @@ Ltac destruct_one_head'_sum := match goal with H : sum _ _ |- _ => destruct H en
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.
+
+Ltac destruct_one_head'_unit := match goal with H : unit |- _ => clear H || destruct H end.
+Ltac destruct_one_head_unit := destruct_one_head'_unit; simpl in *.
+Ltac destruct_head'_unit := repeat destruct_one_head'_unit.
+Ltac destruct_head_unit := repeat destruct_one_head_unit.
+
+Ltac destruct_one_head'_True := match goal with H : True |- _ => clear H || destruct H end.
+Ltac destruct_one_head_True := destruct_one_head'_True; simpl in *.
+Ltac destruct_head'_True := repeat destruct_one_head'_True.
+Ltac destruct_head_True := repeat destruct_one_head_True.
+
+Ltac destruct_one_head'_bool := match goal with H : bool |- _ => clear H || destruct H end.
+Ltac destruct_one_head_bool := destruct_one_head'_bool; simpl in *.
+Ltac destruct_head'_bool := repeat destruct_one_head'_bool.
+Ltac destruct_head_bool := repeat destruct_one_head_bool.