The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

Hello club,

In Tactic Notations one can use lists as arguments, and pass these to 
other tactics that accept lists as arguments, for example:

  Tactic Notation "foo" ident_list(Hs) := revert Hs.

I am wondering whether it is possible to manipulate such lists in Ltac.
For example, could one iterate over these lists, like:

 Tactic Notation "foo" ident_list(Hs) :=
    let rec go Hs :=
      match Hs with
      | nil => idtac
      | ?H :: ?Hs => my_tactic H; go Hs
      end
    in go Hs.

Since I do not know how to do this (and whether it is even possible), I 
often end up writing code like the following:

 Tactic Notation "foo" ident(H1) := my_tactic H1;
 Tactic Notation "foo" ident(H1) ident(H2) :=
   my_tactic H1; my_tactic H2.
 Tactic Notation "foo" ident(H1) ident(H2) ident(H3) :=
   my_tactic H1; my_tactic H2; my_tactic H3.

This obviously does not scale, and becomes very tedious with Tactic 
Notations that take multiple arguments, especially if they take multiple 
lists as arguments.

Best,

Robbert

PS: I often use Coq lists to circumvent this problem, but that only 
works as a replacement for constr_list, but not for arguments of e.g. 
type ident_list or simple_intropattern_list.