feature: notation for lists conforming to the general schema about math-comp HOT 3 CLOSED

Another alternative could be to always use & as the terminator I guess. It would still look more consistent to me.

from math-comp.

The design is that & is the default terminal separator, but other separators can be used when appropriate, so that the notation "reads" better, e.g., [\/ A, B | C] as "A, B or C".
It is important that the terminal separator be symbol that is a separator in the Coq grammar, i.e., that it cannot be construed as an infix operator. Nominally, all sequence items are parsed at level 200 (least binding), so false : l should be parsed as a type cast in your example. So either it is, and you've been saved by some odd error recovery of the stream parser, or you're overriding the cast syntax in manifest sequences, and something like [:: a && b : nat; true] will no longer parse.

from math-comp.

I agree on the aesthetic point, and you gave me a way to explain all this.

from math-comp.