The Coq mailing list

[Chung-Kil Hur <gil.hur AT gmail.com>]

Use appcontext.

Theorem test A (f:A -> A -> Type) (a b :A) :  f a b.
  match goal with
    |- appcontext cxt [ ?g ?x ] => idtac g
  end.

Best,
Gil

On Mon, Nov 28, 2011 at 6:48 AM, Michael Shulman 
<mshulman AT ucsd.edu>
 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.
>
> Thanks!
> Mike
>