The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Daniel Schepler wrote:
> I've defined an induction-like principle for decomposing vectors of positive
> length (just a single decomposition), and I'm trying to define a match-like
> notation to make functions using the principle prettier.  In the attached
> code, the parsing of the notation goes just fine, and the definition of
> vector_decomp gets pretty-printed using the notation.  However, as of Coq
> 8.3pl3, the definitions of vector_hd and vector_tl don't get pretty-printed
> using the notation.  I think maybe the difference is that vector_hd and
> vector_tl have some of the notation's "ident" variables unused in their
> corresponding functions.  It doesn't help to use dummy names for the unused
> variables instead of "_", though.
>
> Is there some way I could define the notation so that it would be used for
> printing in all cases?
>    

The only way I know is to repeat the notation multiple times, once for 
each assignment of values in {used, unused} to all the variable binders 
appearing in the notation.  You can use a character like '?' to 
represent an unused binder.