The Coq mailing list

[Michael Shulman <mshulman AT ucsd.edu>]

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