The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

This is ugly, but works:

Ltac do_work_by rewrite_tac :=

  ...

  rewrite_tac some_eq;

  ... .

Tactic Notation "do_work" := do_work_by ltac:(fun lem => rewrite lem).

Tactic Notation "do_work" "in" hyp(H) := do_work_by ltac:(fun lem => rewrite lem in H).

Tactic Notation "do_work" "in" hyp(H) "|-" := do_work_by ltac:(fun lem => rewrite lem in H |- ).

Tactic Notation "do_work" "in" hyp(H) "|-" "*" := do_work_by ltac:(fun lem => rewrite lem in H |- * ).

Tactic Notation "do_work" "in" "|-" "*" := do_work_by ltac:(fun lem => rewrite lem in H |- * ).

I do not know how to get it to accept an arbitrary number of hypotheses; Coq complains at me if I use [hyp_list].

-Jason

On Mon, Aug 18, 2014 at 4:12 PM, Kirill Taran <kirill.t256 AT gmail.com> wrote:

Hello,

Is there a way to implement tactics polymorphically
relatively to area of tactics effect?
I.e. I want to develop tactic which is possible to use either in goal
or some hypothesis (or both).

E.g. such tactic
  Ltac do_work :=
    ...
    rewrite some_eq (* in H *)
    ... .
which I want to use such way:
  ...
  do_work; do_work in H
  (* bonus: *) do_work in H, <goal>.

Sincerely,
Kirill Taran