The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

A suggestion for a feature that helps one deal with long intro patterns 
containing repeating sequences of "_", "?", etc.

What if each of the intro pattern special symbols could have a repeat 
count?  For instance, instead of:

  intros _ _ _ _ _ _ _ x _ _ _ _ y.

Have:

  intros 7 _  x 4 _ y.

where these repeat counts are only for parsing.  For extra credit, allow 
repeated subpatterns:

  intros (? 8 (& ?)).

instead of

  intros (? & ? & ? & ? & ? & ? & ? & ? & ?).

-- Jonathan