coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] about Tactic Notation: a variant of apply ... with ...

From: Gyesik Lee <gslee AT ropas.snu.ac.kr>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] about Tactic Notation: a variant of apply ... with ...
Date: Mon, 19 Jul 2010 14:50:32 +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=o986KSkGL2L/+NfXNgaYkcB8ddp6VOf2nIopGGPX7n93C3G/5IV0nlL2HSvZhw8PGH K4yOaSXBlGCgGs9rzVxNumFHf6JukYW5ditIro61s+rpiwsjgvRLWo0k/D5dQa6UtQ1E Fs7oRTC9QYBik/qv2GOKOu7vWRjegU6t+NEr0=

Hi,

How can I write a tactic with a binding list as in the case of "apply
... with ..." ?

I am wondering which tactic argument can be used in the following example
case:

Tactic Notation "papply" constr(H) "with" ???(a:=x)
:= simpl; apply H with (a:=x)

Any help will be greatly appreciated.

Gyesik

[Coq-Club] about Tactic Notation: a variant of apply ... with ..., Gyesik Lee
- Message not available
  - Re: [Coq-Club] about Tactic Notation: a variant of apply ... with ..., Gyesik Lee
    - Re: [Coq-Club] about Tactic Notation: a variant of apply ... with ..., AUGER C�dric
    - Message not available
      - Re: [Coq-Club] about Tactic Notation: a variant of apply ... with ..., Gyesik Lee
        
        Re: [Coq-Club] about Tactic Notation: a variant of apply ... with ..., Arthur Charguéraud
        
        Re: [Coq-Club] about Tactic Notation: a variant of apply ... with ..., Gyesik Lee
    - Re: [Coq-Club] about Tactic Notation: a variant of apply ... with ..., AUGER Cedric