The Coq mailing list

[Pierre Letouzey <pierre.letouzey AT inria.fr>]

----- Mail original -----
> On Mon, Nov 28, 2011 at 4:15 PM, Chung-Kil Hur 
>Â <gil.hur AT gmail.com>
> wrote:
> > 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.
> 
> That might be a great thing to add to the documentation :)

Done in the svn :)
Best,
Pierre