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