The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Wednesday, June 18, 2014 02:10:36 PM Arnaud Spiwack wrote:
> is that t;[t1|…|tn] is *not* of the form t;t'. It is easily witnessed in
> that t;([t1|…|tn]) is not parsable. I could fix the problem by introducing
> a syntax [t1|…|tn] and make it so that ; [ is parsed specially and that we
> have to write t;([t1|…|tn]) to the the simple semantics. But I fear the
> complaints would be loud.

What if [t1|...|tn] meant: fail if the number of focused goals is not a 
multiple of n; and if it is a multiple of n, apply t1, ..., tn round robin to 
the focused goals.
-- 
Daniel Schepler