diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-12-04 15:37:51 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-12-04 15:37:51 -0500 |
| commit | e6044c2fe0cc7b5662076bb1f26342a4d590132e (patch) | |
| tree | ab67a9fff8bee7744cdc444f79ae197310c733f3 /src/Util/Tactics/DestructHyps.v | |
| parent | b60db17b237fc5df0e1606d55d7056e9e11b10ea (diff) | |
Add inversion_clear tactics
Diffstat (limited to 'src/Util/Tactics/DestructHyps.v')
| -rw-r--r-- | src/Util/Tactics/DestructHyps.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/Util/Tactics/DestructHyps.v b/src/Util/Tactics/DestructHyps.v index 8ab6215c2..43f578291 100644 --- a/src/Util/Tactics/DestructHyps.v +++ b/src/Util/Tactics/DestructHyps.v @@ -30,6 +30,11 @@ 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 * ). @@ -39,6 +44,10 @@ 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 |