diff options
Diffstat (limited to 'src/Util/Tactics/DestructHead.v')
-rw-r--r-- | src/Util/Tactics/DestructHead.v | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/src/Util/Tactics/DestructHead.v b/src/Util/Tactics/DestructHead.v index 5620a72c9..fa7693e5e 100644 --- a/src/Util/Tactics/DestructHead.v +++ b/src/Util/Tactics/DestructHead.v @@ -27,3 +27,34 @@ Ltac destruct_head_hnf' T := destruct_all_matches' ltac:(head_hnf_matcher T). Ltac inversion_head_hnf T := inversion_all_matches ltac:(head_hnf_matcher T). Ltac inversion_one_head_hnf T := inversion_one_match ltac:(head_hnf_matcher T). Ltac inversion_head_hnf' T := inversion_all_matches' ltac:(head_hnf_matcher T). + +(** Faster versions for some common connectives *) +Ltac destruct_one_head'_ex := match goal with H : ex _ |- _ => destruct H end. +Ltac destruct_one_head_ex := destruct_one_head'_ex; simpl in *. +Ltac destruct_head'_ex := repeat destruct_one_head'_ex. +Ltac destruct_head_ex := repeat destruct_one_head_ex. + +Ltac destruct_one_head'_sig := match goal with H : sig _ |- _ => destruct H end. +Ltac destruct_one_head_sig := destruct_one_head'_sig; simpl in *. +Ltac destruct_head'_sig := repeat destruct_one_head'_sig. +Ltac destruct_head_sig := repeat destruct_one_head_sig. + +Ltac destruct_one_head'_sigT := match goal with H : sigT _ |- _ => destruct H end. +Ltac destruct_one_head_sigT := destruct_one_head'_sigT; simpl in *. +Ltac destruct_head'_sigT := repeat destruct_one_head'_sigT. +Ltac destruct_head_sigT := repeat destruct_one_head_sigT. + +Ltac destruct_one_head'_prod := match goal with H : prod _ _ |- _ => destruct H end. +Ltac destruct_one_head_prod := destruct_one_head'_prod; simpl in *. +Ltac destruct_head'_prod := repeat destruct_one_head'_prod. +Ltac destruct_head_prod := repeat destruct_one_head_prod. + +Ltac destruct_one_head'_and := match goal with H : and _ _ |- _ => destruct H end. +Ltac destruct_one_head_and := destruct_one_head'_and; simpl in *. +Ltac destruct_head'_and := repeat destruct_one_head'_and. +Ltac destruct_head_and := repeat destruct_one_head_and. + +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. |