coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] appcontext question

From: Dmitry Grebeniuk <gdsfh1 AT gmail.com>
To: Jason Gross <coq-club AT inria.fr>
Subject: Re: [Coq-Club] appcontext question
Date: Wed, 13 Mar 2013 14:32:33 +0200

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?

[Coq-Club] appcontext question, Dmitry Grebeniuk, 03/11/2013
- Re: [Coq-Club] appcontext question, Adam Chlipala, 03/11/2013
  - Re: [Coq-Club] appcontext question, Jason Gross, 03/11/2013
    - Re: [Coq-Club] appcontext question, Dmitry Grebeniuk, 03/13/2013
      - Re: [Coq-Club] appcontext question, Jason Gross, 03/13/2013
  - Re: [Coq-Club] appcontext question, Dmitry Grebeniuk, 03/13/2013
    - Re: [Coq-Club] appcontext question, Adam Chlipala, 03/13/2013