diff options
author | Jason Gross <jgross@mit.edu> | 2018-09-27 15:13:43 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2018-09-27 15:13:43 -0400 |
commit | d6c9be90fbcb0b41f02f1de8d872ef4b04446d6f (patch) | |
tree | 67bc7b8ef07abf1b72d96992ceb4beb02dc9bb10 /src/Util/Tactics/DestructHead.v | |
parent | c6a0e469374bbdc67366894c87d1150be1445d40 (diff) |
Add destruct_head_{False,Empty_set}
Diffstat (limited to 'src/Util/Tactics/DestructHead.v')
-rw-r--r-- | src/Util/Tactics/DestructHead.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/Util/Tactics/DestructHead.v b/src/Util/Tactics/DestructHead.v index 94c1d601a..c5c8a86bc 100644 --- a/src/Util/Tactics/DestructHead.v +++ b/src/Util/Tactics/DestructHead.v @@ -78,3 +78,13 @@ Ltac destruct_one_head'_bool := match goal with H : bool |- _ => clear H || dest 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. + +Ltac destruct_one_head'_False := match goal with H : False |- _ => destruct H end. +Ltac destruct_one_head_False := destruct_one_head'_False; simpl in *. +Ltac destruct_head'_False := repeat destruct_one_head'_False. +Ltac destruct_head_False := repeat destruct_one_head_False. + +Ltac destruct_one_head'_Empty_set := match goal with H : Empty_set |- _ => destruct H end. +Ltac destruct_one_head_Empty_set := destruct_one_head'_Empty_set; simpl in *. +Ltac destruct_head'_Empty_set := repeat destruct_one_head'_Empty_set. +Ltac destruct_head_Empty_set := repeat destruct_one_head_Empty_set. |