coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] How do I write tactic notations accepting one or two tactic arguments?
Date: Thu, 19 Jun 2014 15:34:31 +0100

Hi,

I can't seem to figure out how to get the following tactic notations to work. Can someone enlighten me as to what's going wrong?

Tactic Notation "basicapply" open_constr(R) "using" tactic(tac) "and" tactic(tacfin) := idtac.

Tactic Notation "basicapply" open_constr(R) "using" tactic(tac) := basicapply R using tac and idtac.

(* Toplevel input, characters 99-100:

Syntax error: 'and' expected after [tactic:tactic] (in [tactic:simple_tactic]). *)

Thanks,

Jason

[Coq-Club] How do I write tactic notations accepting one or two tactic arguments?, Jason Gross, 06/19/2014
- Re: [Coq-Club] How do I write tactic notations accepting one or two tactic arguments?, Cedric Auger, 06/19/2014
  - Re: [Coq-Club] How do I write tactic notations accepting one or two tactic arguments?, Jason Gross, 06/19/2014