The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi,
I guess Ltac functions are not macros, they define new tactics
considered as one single step by tacticals.

If you define a macro:

Tactic Notation "prgt3" int(t1) int(t2) :=  prgt t1 ; prgt t2.

then it works as expected.

P.

Le lun. 28 janv. 2019 à 09:40, Jeremy Dawson
<Jeremy.Dawson AT anu.edu.au>
 a écrit :
>
> Yes, it seems that this is the case in the example below.  I'm trying to
> understand why.
>
> In the example below I would have expected that
> split ; (prgt 22 ; prgt 33).
> and
> split ; (prgt2 22 33).
> would have the same result, but they don't.
>
> Why is this?
>
> Thanks
>
> Jeremy
>
> On 01/23/2019 09:18 PM, Théo Zimmermann wrote:
> >
> >     In https://coq.inria.fr/refman/proof-engine/ltac.html
> >     under Semantics then under Sequence it says
> >     Sequence is associative.
> >
> >     I would take that to mean that
> >     (tac1 ; tac2) ; tac3
> >     is the same as
> >     tac1 ; (tac2 ; tac3)
> >
> >     But is this so?
> >
> >
> > The order would be the same in both cases.
>
> Yes, it seems that this is the case in the example below.  I'm trying to
> understand why.
>
> In the example below I would have expected that
> split ; (prgt 22 ; prgt 33).
> and
> split ; (prgt2 22 33).
> would have the same result, but they don't.
>
> Why is this?
>
> Thanks
>
> Jeremy
>
> Ltac prgt t :=
>    match goal with
>      | [ |- ?P ] => idtac t P
>      end.
>
> Ltac prgt2 t1 t2 := prgt t1 ; prgt t2.
>
> Variable P : Prop.
> Variable Q : Prop.
> Goal P /\ Q.
>
> (split ; prgt 22) ; prgt 33.
> Undo.
> split ; (prgt 22 ; prgt 33).
> Undo.
> split ; (prgt2 22 33).