The Coq mailing list

[Ilya Sergey <ilya.sergey AT imdea.org>]

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 *)
    ... .

If the only purpose of the tactic is to do rewriting by propositional equality then I'd recommend to take a look at SSReflect's extended rewriting, as it seem to do exactly what you need, namely, perform rewriting in an arbitrary number of hypotheses and (optionally) a goal.

Cheers,

Ilya