# Applying custom tactic in hypothesis

To avoid tedious repetition I have a tactic that looks something like this:

Ltac unfolds := try unfold foo;
try unfold bar;
try unfold baz;
apply some_lemma.


However, sometimes the expressions I would like to unfold are not in the goal, but in the hypotheses. I can make another tactic

Ltac unfolds' H := try unfold foo in H;
try unfold bar in H;
try unfold baz in H;
apply some_lemma in H.


but is there a way to write my tactic so that it can (optionally) be used in hypotheses?

ie. so that I can write unfolds in H. in my proofs

I believe replacing your definition of unfolds' with
Tactic Notation "unfolds" "in" hyp(H) := ... should work. That's how stdpp defines a similar tactic (see line 305 in https://gitlab-10.mpi-sws.org/iris/stdpp/-/blob/master/stdpp/tactics.v.) You still have to define the tactic twice, once for the goal and once for hypotheses, but you should be able to use it in the way you want.