The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Mon, Jun 17, 2013 at 03:01:30PM +0200, Robbert Krebbers wrote:
>   rewrite foo; rewrite bar; rewrite baz

I guess this line is equivalent to "rewrite foo bar baz" in ssreflect,
but not to "rewrite foo, bar, baz" in standard Coq (if one of the rewrite
rules generates a side goal for example).

> Doesn't ssreflect have syntax for that? How about borrowing that?

Ssreflect's syntax supports reversing the list of subgoals or rotating
this list back and forward.  This is clearly sufficient for short lists
of goals (as it is often the case in the MathComp library), but may not
be as general as Arnaud wants it.
Anyway it is documented here: http://hal.inria.fr/inria-00258384 page 37.

Cheers
-- 
Enrico Tassi