The Coq mailing list

["Carlos.SIMPSON" <carlos AT math.unice.fr>]

I would like to second Lukasz Stafiniak's suggestions (as I imagine
would a lot of people).
Here is a little addition (although maybe that was meant as a part of
the third one):
it would be nice to have a command to apply something once to each
element of the context,
such as
Cycle Context With
[id1 : ?1 |- ?] -> Dosomething

then it would apply (as in Repeat) the tactic Dosomething, once for each
identifier in the context.

One can do this type of thing by hacking with the present language but
it is really ugly.

---Carlos