From d6c9be90fbcb0b41f02f1de8d872ef4b04446d6f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 27 Sep 2018 15:13:43 -0400 Subject: Add destruct_head_{False,Empty_set} --- src/Util/Tactics/DestructHead.v | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'src/Util') 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. -- cgit v1.2.3