Applying custom tactic in hypothesis

Question

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

Answer 1

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.