Adding "in" part to tactic to specify where to apply it

Question

I am new to Coq and to writing tactics, and I have been unable to figure out whether you can define more complicated tactics like the build in ones. For example, say that I have a tactic tac1 taking two arguments, and I define tac2 by

Ltac tac2 arg := tac1 arg _.

Then this works as I would expect, but I would really like to be able to call tac2 on a hypothesis, like tac2 arg in H. I can see that I can just give the hypothesis as an extra argument, but then I cannot use it in the goal, and I would also like to be able to use it like tac2 arg in *.

Is something like that possible, and how would it be accomplished?

I have found this answer about how you add intro patterns to tactics you define, and it lead me to this page about Tactic Notation, but I am unable to figure out from that if what I would like is possible.

Answer 1

Following this answer, you may define notations for tac2 like this:

Tactic Notation "tac2" constr(arg) :=
  tac1 arg _.

Tactic Notation "tac2" constr(arg) "in" hyp(H) :=
  tac1 arg _ in H.

Tactic Notation "tac2" constr(arg) "in" "*" :=
  repeat match goal with
         | H:_ |- _ => tac2 arg in H
         | |- _ => tac2 arg
         end.

Of course, tac1 needs to work with an in modifier and you should be careful with the termination of the repeat (see here).