The Coq mailing list

[Kirill Taran <kirill.t256 AT gmail.com>]

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