The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Indeed, "basicapply R using (tac) and idtac" works.  Why do the parentheses do something here?

Thanks,

Jason

On Thu, Jun 19, 2014 at 5:34 PM, Cedric Auger <sedrikov AT gmail.com> wrote:

I am not expert in tactic notations, but maybe that the problem is that "basicapply R using tac and idtac" is parsed as:
"basicapply" open_constr(R)=<R> "using" tactic(tac)=<tac and idtac>
instead of:
"basicapply" open_constr(R)=<R> "using" tactic(tac)=<tac> "and" tactic(tacfin)=<idtac>

I have no Coq installation, so I cannot try to see if "basicapply R using (tac) and idtac" works better.

2014-06-19 16:34 GMT+02:00 Jason Gross <jasongross9 AT gmail.com>:

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

--
.../Sedrikov\...