coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] match goal with "match ... with"

From: Gyesik Lee <gslee AT ropas.snu.ac.kr>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] match goal with "match ... with"
Date: Fri, 2 Jul 2010 22:04:31 +0900
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:date:x-google-sender-auth:message-id:subject :from:to:content-type; b=HYycMmUkj1F+PF1DTepyCBB2u0RYLmvN401yRcPvfr2O4iykzUKDzRNzOdOa3cZsfv 4p8YOh5Zpua1C+3cBrKNc2fa5wj0cQTN8vhTVvLj29StGxgasrrmwRZTJKmm2PnnCOqN xPwmK2KeCL1i/th79M41A0PK68y/33XmCcksM=

Hi,

I am wondering how to use "match goal with" with context option in the
following case:

Ltac toto :=
  match goal with
     | |- context [ match ?T with ] => idtac
  end

But Coq complains as follows:

Syntax error: [branches] expected after 'with' (in [match_constr]).

Then I tried with

Ltac toto :=
  match goal with
     | |- context [ match ?T with | _ => _ end ] => idtac
  end

The error message now:

Error: Non supported pattern.

I guess it is because of special meaning of "match T with" as a Coq
vernacular.
Any kind of help will be appreciated.

Gyesik

[Coq-Club] match goal with "match ... with", Gyesik Lee
- Re: [Coq-Club] match goal with "match ... with", Adam Chlipala
  - Re: [Coq-Club] match goal with "match ... with", Gyesik Lee
    - Re: [Coq-Club] match goal with "match ... with", Adam Chlipala