The Coq mailing list

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

Michael Shulman wrote:
> Why does the following match fail?
>
> Theorem test A (f:A ->  A ->  Type) (a b :A) :  f a b.
>    match goal with
>      |- context cxt [ ?g ?x ] =>  idtac g
>    end.
>
> It looks to me as though the goal contains two subterms of the form (g
> x), one where g = f and x = a, and another where g = (f a) and x = b.
>    

Until recently, that example would fail even without the [context] 
pattern.  My guess is that [context] isn't implemented to consider all 
prefixes of a curried application as separate terms.  (The internal 
representation of terms combines curried applications into single terms, 
so it takes extra work to get behavior that matches our informal idea of 
the syntax.)

A standard trick which seems hacky but imposes minimal hassle in 
practice is to include a pattern for every function arity you want to 
support.