The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Gyesik Lee wrote:
> > 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.
> >      
> Does this mean that
>
>    
> > >    match goal with
> > >       | |- context [ match ?T with | _ =>   _ end ] =>   idtac
> > >    end
> > >        
> can be used only in a proof, and not as a standing-alone tactic with a name?
>    

That Ltac code is not legal anywhere, with or without a name.  Try it 
and you'll see.