The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I'm not sure if it's a bug, but I've filed a bug report at https://coq.inria.fr/bugs/show_bug.cgi?id=3002; even if it's not a bug, the documentation should talk about this behavior.

-Jason

On Wed, Mar 13, 2013 at 8:32 AM, Dmitry Grebeniuk <gdsfh1 AT gmail.com> wrote:

Hello.

> There is an oddity when your head is a hole; I'm not sure what to make of
> it.  For example,
> Goal 1 + 2 = 3.
> match goal with
>   | [ |- context[_ 2] ] => pose 0 (* succeeds *)
> end.
>
> Goal 1 + (id 2) = 3.
> match goal with
>   | [ |- context[_ (id 2)] ] => pose 0 (* fails *)
> end.

  This looks strange.  Should I file a bug report,
or this is the correct behaviour?