The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Eugene Kirpichov wrote:
> 2010/1/30 Adam 
> Chlipala<adam AT chlipala.net>:
>    
> > Eugene Kirpichov wrote:
> >      
> > > Suppose I'm proving the following theorem.
> > > Theorem t : forall n, match n with | O =>    O | S x =>    S x end = n.
> > >    intros n.
> > >        
> Thanks, but the following statement also doesn't work.
>
>    match goal with [ |- match ?n with | O =>  _ | S _ =>  _ end ] =>
> destruct n end.
>    

Your goal isn't a [match].  Rather, your goal is an equality whose 
lefthand side is such a [match].  You can add [= _] to your pattern or 
use a [context] pattern.

> By the way, I still don't understand why Coq needs type information in
> this case, if Ltac is untyped and operates over syntax...
>    

It's clear if you look at Coq's kernel representation of Gallina 
programs, where a [match] contains an array of cases, one per 
constructor, regardless of which patterns were entered at the source 
level.  I agree that this isn't very convenient from the user's perspective.