Ltac with variadic argument

Using Coq
1

Hello,
I am trying to write a tactic that wraps around rewrite, like this:

Ltac sire H := simpl; rewrite H; simpl.

However, rewrite is variadic, but it seems that

sire hyp1, hyp2.

is rejected by Coq since it only expects one argument. I would expect it to expand something like

simpl; rewrite hyp1, hyp2; simpl.

Is there any way to do this in Ltac?
(I have found this coq - Tactics with variable arity - Stack Overflow but the links are dead and it is not very clear)

Best,
Mrandl

3

I thought this would work:

Ltac rew l := rewrite l.

Tactic Notation (at level 3) "sss" ne_constr_list_sep(l,",") :=
  (simpl; rew l ; simpl).

Lemma foo: forall x y z:nat, x = y -> y = 0 + z -> 0 + x = z.
Proof.
  intros x y z hyp1 hyp2. 
  sss hyp1,hyp2.

But for some reason it doesn’t. Probably because rewrite takes something more complex than just a list of terms.

1 Like