The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

On 06/17/2013 10:34 AM, Arnaud Spiwack wrote:
> There is indeed: rewrites at least are supposed to be chained, even when
> they have side conditions. It's easier to chain them if the main goal is
> the first one
I do not see why. In case of chained rewrites of the form

  rewrite foo, bar, baz

that should just be an implementation problem, not a problem for the end 
user. In case of

  rewrite foo; rewrite bar; rewrite baz

the consecutive rewrites are applied to all sub goals (including the 
subgoals of the side conditions).

> And on a related note, I still haven't brought myself to write a tactic
> to reorder goals. Mostly because I haven't settled on the syntax.
Doesn't ssreflect have syntax for that? How about borrowing that?

Robbert