diff options
Diffstat (limited to 'src/Util/Tactics.v')
| -rw-r--r-- | src/Util/Tactics.v | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index aa8093308..8ddfecb5f 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -302,6 +302,26 @@ Tactic Notation "rewrite_hyp" "!*" "in" "*" := progress rewrite_hyp ?* in *. Tactic Notation "rewrite_hyp" "->" "!*" "in" "*" := progress rewrite_hyp -> ?* in *. Tactic Notation "rewrite_hyp" "<-" "!*" "in" "*" := progress rewrite_hyp <- ?* in *. +Tactic Notation "erewrite_hyp" "*" := do_with_hyp' ltac:(fun H => erewrite H). +Tactic Notation "erewrite_hyp" "->" "*" := do_with_hyp' ltac:(fun H => erewrite -> H). +Tactic Notation "erewrite_hyp" "<-" "*" := do_with_hyp' ltac:(fun H => erewrite <- H). +Tactic Notation "erewrite_hyp" "?*" := repeat do_with_hyp' ltac:(fun H => erewrite !H). +Tactic Notation "erewrite_hyp" "->" "?*" := repeat do_with_hyp' ltac:(fun H => erewrite -> !H). +Tactic Notation "erewrite_hyp" "<-" "?*" := repeat do_with_hyp' ltac:(fun H => erewrite <- !H). +Tactic Notation "erewrite_hyp" "!*" := progress erewrite_hyp ?*. +Tactic Notation "erewrite_hyp" "->" "!*" := progress erewrite_hyp -> ?*. +Tactic Notation "erewrite_hyp" "<-" "!*" := progress erewrite_hyp <- ?*. + +Tactic Notation "erewrite_hyp" "*" "in" "*" := do_with_hyp' ltac:(fun H => erewrite H in * ). +Tactic Notation "erewrite_hyp" "->" "*" "in" "*" := do_with_hyp' ltac:(fun H => erewrite -> H in * ). +Tactic Notation "erewrite_hyp" "<-" "*" "in" "*" := do_with_hyp' ltac:(fun H => erewrite <- H in * ). +Tactic Notation "erewrite_hyp" "?*" "in" "*" := repeat do_with_hyp' ltac:(fun H => erewrite !H in * ). +Tactic Notation "erewrite_hyp" "->" "?*" "in" "*" := repeat do_with_hyp' ltac:(fun H => erewrite -> !H in * ). +Tactic Notation "erewrite_hyp" "<-" "?*" "in" "*" := repeat do_with_hyp' ltac:(fun H => erewrite <- !H in * ). +Tactic Notation "erewrite_hyp" "!*" "in" "*" := progress erewrite_hyp ?* in *. +Tactic Notation "erewrite_hyp" "->" "!*" "in" "*" := progress erewrite_hyp -> ?* in *. +Tactic Notation "erewrite_hyp" "<-" "!*" "in" "*" := progress erewrite_hyp <- ?* in *. + (** Execute [progress tac] on all subterms of the goal. Useful for things like [ring_simplify]. *) Ltac tac_on_subterms tac := repeat match goal with |