The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Gyesik Lee wrote:
> Then I tried with
>
> Ltac toto :=
>    match goal with
>       | |- context [ match ?T with | _ =>  _ end ] =>  idtac
>    end
>
> The error message now:
>
> Error: Non supported pattern.
>    

For now, you need to supply every pattern-match case, in enough detail 
to make clear which type you're matching on.  It gets bothersomely 
verbose and prevents genericity, but it makes some sense if you look at 
the internal representation of Gallina terms.