Tactics with variable arity

Question

Say I want to have a tactic to clear multiple hypothesis at once, to do something like clear_multiple H1, H2, H3.. I tried to do that using pairs, like the following:

Ltac clear_multiple arg :=
match arg with
| (?f, ?s) => clear s; clear_multiple f
| ?f => clear f
end.

But then, the problem is that I have to place parenthesis to have a Prod:

Variable A: Prop.

Goal A -> A -> A -> True.
intros.
clear_multiple (H, H0, H1).

My question is, how to do that without using Prods ?

---

I checked this question, but it is not exactly what I want, since the number of arguments I want is not known.

Answer 1

You might like to know that the clear tactic can take multiple arguments, so you do not need to define a new tactic: you can just write clear H H0 H1.

Of course, you might want to define such n-ary tactics for other tasks. Coq has a tactic notation mechanism that supports such definitions. Unfortunately, they are not too powerful: you can only pass a list of arguments of a certain kind to a tactic that expects multiple arguments (like clear); I don't think it can give you a list that you can iterate on programmatically.