The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

This might have worked (though I find it a bit bizarre). But I don't see it being compatible with the full syntax a;[b1|…|bk|c..|d1|…|dn]  (note how the double period is, confusingly enough, part of the syntax). It means: do a, which will produce at least k+n goals, apply b1…bk to the k first, d1…dn to the n last, and c to each one in the middle.

On 18 June 2014 17:31, Daniel Schepler <dschepler AT gmail.com> wrote:

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