From abed3aa12aa0e754f453b1fd5c4ab59c75137df5 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 4 Dec 2018 15:43:49 -0500 Subject: Revert "Add inversion_clear tactics" This reverts commit e6044c2fe0cc7b5662076bb1f26342a4d590132e. Actually not needed; the tactics already clear the relevant hypotheses. --- src/Util/Tactics/DestructHead.v | 8 -------- src/Util/Tactics/DestructHyps.v | 9 --------- 2 files changed, 17 deletions(-) (limited to 'src/Util') diff --git a/src/Util/Tactics/DestructHead.v b/src/Util/Tactics/DestructHead.v index bfe615f10..c5c8a86bc 100644 --- a/src/Util/Tactics/DestructHead.v +++ b/src/Util/Tactics/DestructHead.v @@ -15,10 +15,6 @@ Ltac inversion_head T := inversion_all_matches ltac:(destruct_head_matcher T). Ltac inversion_one_head T := inversion_one_match ltac:(destruct_head_matcher T). Ltac inversion_head' T := inversion_all_matches' ltac:(destruct_head_matcher T). -Ltac inversion_clear_head T := inversion_clear_all_matches ltac:(destruct_head_matcher T). -Ltac inversion_clear_one_head T := inversion_clear_one_match ltac:(destruct_head_matcher T). -Ltac inversion_clear_head' T := inversion_clear_all_matches' ltac:(destruct_head_matcher T). - Ltac head_hnf_matcher T HT := match head_hnf HT with @@ -32,10 +28,6 @@ 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). -Ltac inversion_clear_head_hnf T := inversion_clear_all_matches ltac:(head_hnf_matcher T). -Ltac inversion_clear_one_head_hnf T := inversion_clear_one_match ltac:(head_hnf_matcher T). -Ltac inversion_clear_head_hnf' T := inversion_clear_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 *. diff --git a/src/Util/Tactics/DestructHyps.v b/src/Util/Tactics/DestructHyps.v index 43f578291..8ab6215c2 100644 --- a/src/Util/Tactics/DestructHyps.v +++ b/src/Util/Tactics/DestructHyps.v @@ -30,11 +30,6 @@ Ltac inversion_all_matches_then matcher tac := Ltac inversion_one_match_then matcher tac := do_one_match_then matcher ltac:(fun H => inversion H; subst) tac. -Ltac inversion_clear_all_matches_then matcher tac := - do_all_matches_then matcher ltac:(fun H => inversion H; clear H; subst) tac. -Ltac inversion_clear_one_match_then matcher tac := - do_one_match_then matcher ltac:(fun H => inversion H; clear H; subst) tac. - Ltac destruct_all_matches matcher := destruct_all_matches_then matcher ltac:( simpl in * ). Ltac destruct_one_match matcher := destruct_one_match_then matcher ltac:( simpl in * ). @@ -44,10 +39,6 @@ Ltac inversion_all_matches matcher := inversion_all_matches_then matcher ltac:( Ltac inversion_one_match matcher := inversion_one_match_then matcher ltac:( simpl in * ). Ltac inversion_all_matches' matcher := inversion_all_matches_then matcher idtac. -Ltac inversion_clear_all_matches matcher := inversion_clear_all_matches_then matcher ltac:( simpl in * ). -Ltac inversion_clear_one_match matcher := inversion_clear_one_match_then matcher ltac:( simpl in * ). -Ltac inversion_clear_all_matches' matcher := inversion_clear_all_matches_then matcher idtac. - (* matches anything whose type has a [T] in it *) Ltac destruct_type_matcher T HT := match HT with -- cgit v1.2.3