coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] minimal example for "tac; tac in H; tac in *"

From: Jason Gross <jasongross9 AT gmail.com>
To: t x <txrev319 AT gmail.com>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] minimal example for "tac; tac in H; tac in *"
Date: Wed, 14 Aug 2013 12:38:05 -0400

You're looking for the "Tactic Notation" vernacular command.

-Jason

On Wednesday, August 14, 2013, t x wrote:

Hi,

Can someone point me at documentation / minimal example (or even the right keyword to google for this) for designing a Ltac

Ltac tac := ...

s.t.

"tac;" --> idtac "case 0"
"tac in H;" --> idtac H;
"tac in *;" --> idtac "all"

Thanks!

[Coq-Club] minimal example for "tac; tac in H; tac in *", t x, 08/14/2013
- Re: [Coq-Club] minimal example for "tac; tac in H; tac in *", Jason Gross, 08/14/2013
  - Re: [Coq-Club] minimal example for "tac; tac in H; tac in *", t x, 08/15/2013