diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-12-04 15:43:49 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-12-04 15:43:49 -0500 |
| commit | abed3aa12aa0e754f453b1fd5c4ab59c75137df5 (patch) | |
| tree | 92b5afd11d8a4dcbdc0df1b89e6a67d2b5464141 /src/Util/Tactics/DestructHead.v | |
| parent | e6044c2fe0cc7b5662076bb1f26342a4d590132e (diff) | |
Revert "Add inversion_clear tactics"
This reverts commit e6044c2fe0cc7b5662076bb1f26342a4d590132e.
Actually not needed; the tactics already clear the relevant hypotheses.
Diffstat (limited to 'src/Util/Tactics/DestructHead.v')
| -rw-r--r-- | src/Util/Tactics/DestructHead.v | 8 |
1 files changed, 0 insertions, 8 deletions
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 *. |