Julien Cretin

> > SELF at the beginning of a production seems to always mean "SELF except rules that start with SELF" which contradicts that is currently documented. > > That doesn't...

> the `foo!` notation starts with SELF and still works on the left of `+` Yes, that's what I told @proux01 in https://github.com/rocq-prover/rocq/pull/21071#discussion_r2327661869

I think the first step would be to describe what the current implementation does and ideally when it started differing from how Camlp5 handles associativity (which is what is currently...

> "continue" does not mean "recovery" Then what is "recovery"?

Ok so it's closely related because what you consider outside the grammar directly depends on whether SELF on the left means SELF (what seems to be the current state) or...

Yes I know, I'm saying that if `!` were at level 92 I would also consider this outside the grammar, because `x` is at level 91 in `x #` (according...

> I'm not sure that ever changed. It just seems that the doc is wrong. I see. And this wrongness would have be copied to `Print Notation`. I guess that's...

> However, if the left SELF of "minus" there were to be NEXT, there is no way "-" could be parsed in a left-associative way. Search for "in the left...

> The left SELF calls the "start" parser of the current level Thanks! If I cross this information with what Pierre said in https://github.com/rocq-prover/rocq/pull/21071#discussion_r2333446061 I suspect that the "start" parser...

Yes, SELF on the left is somewhere between NEXT and SELF, which in the top comment I called `norec(SELF)` (from your `ltac_expr2_norec` suggestion). Also curious how much would break.