me again ...
I found that the precedence of
assert x by y; z seems to be different from Ltac1. As far as I can tell Ltac2 interprets
assert x by y; z as
assert x by (y; z) while Ltac interprets it as
(assert x by y); z. Is this intentional?
Not that I know of.
Some precedences related to application were voluntarily changed, e.g. try and friends
But this one looks like a bug (?)
It's quite easy to fix, there is a clear difference between the Ltac1 and Ltac2 entry in this case.
(a missing level, as expected)
OK, thanks! Should I create an issue?
by would also read
by (foo ; bar ; baz)
According to my experience, this is what you want most of the times. (at least in interactive scripts)
And it's precedence is always the same, it does not depend on what it follows
I just double checked Ltac1 again. It is indeed different as this snippet shows:
Goal 1=1. Fail assert (1=1) by idtac; reflexivity. assert (1=1) by (idtac; reflexivity).
So what shall we do? Make Ltac2 ssreflect compatible or Ltac compatible? I have no strong opinion on this. When it comes to non trivial tactics, they are all anyway quite different.
There are btw. a few other precedence differences, e.g. around repeat. Is the expectation that Ltac2 mimics Ltac as much as possible and deviations shall be reported?
The change of parsing for repeat is voluntary.
It's an issue many people have complained about for a long time.
(I mean, for Ltac1.)
So I decided for it to be a salient breakage introduced by Ltac2.
try and similarly one-identifier tacticals.
They now all behave as if they were function applications (modulo the implicit thunk introduced by the syntactic notation)
Last updated: Jan 31 2023 at 09:01 UTC