diff options
| author |  Jason Gross <jagro@google.com> | 2016-08-08 11:00:35 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-08-08 11:00:35 -0700 |
| commit | 117b11817e21a48aeec424c805676bbde3d96f71 (patch) | |
| tree | 7440be2d5f6477dd6ba9788c5b80b35e357c3de4 /src/Util/Tactics.v | |
| parent | f1796582647d9530eae9d36b85d8c9b749f39635 (diff) | |
Add erewrite_hyp tactics
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 |