coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Strange Ltac behavior

From: Thomas Braibant <thomas.braibant AT gmail.com>
To: Aaron Bohannon <bohannon AT cis.upenn.edu>
Cc: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Strange Ltac behavior
Date: Wed, 23 Feb 2011 21:58:18 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; b=LbcUbo5+VDHudTneNJT6I3F2sXoIEIAeYEEj7XsZcARQN/ETVPWyMhElbFiK5HFmLN v3byD9AjToeHLaqOJGojT2jNKnZ7mYWRD0S728yHKQIks0v2mMCXU9PNL0LX2diT94wb EQyMxqUbEJwxSfOVyRd4ewtvysc7aY1FHBB8M=

On Wed, Feb 23, 2011 at 9:39 PM, Aaron Bohannon
<bohannon AT cis.upenn.edu>
wrote:
> Alternatively, instead of using a nested match, you can use
> "constr_eq", which compares the ASTs of the terms. �So you can do
> something like this:
>
> match goal with
> | v : T ?n |- context name [?v1] => �constr_eq v v1; idtac v
> end.
>

Nice solution, and thanks to both.

Thomas

[Coq-Club] Strange Ltac behavior, Thomas Braibant
- Re: [Coq-Club] Strange Ltac behavior, Adam Chlipala
  - Re: [Coq-Club] Strange Ltac behavior, Aaron B.
    - Re: [Coq-Club] Strange Ltac behavior, Aaron Bohannon
      - Re: [Coq-Club] Strange Ltac behavior, Thomas Braibant
        
        Re: [Coq-Club] Strange Ltac behavior, Aaron Bohannon