The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

I should have read the documentation before replying, the simplest way
to do what you wanted seemed to be:

Tactic Notation "sapply" constr(H) "with" constr_list(list) :=
simpl; apply  H with list.

I tried it, it is recognized, but I didn't tested it.
But if you need to preprocess your list using custom tactics, it won't
work.

I also tried Arthur workaround some time ago, it worked, but it is
not very pretty to see, and using coq structures at tactical language
is not very clean as you use tokens of a language in a meta-language
over the one of where your tokens are…