Sorry, another question about Ltac2 Notations.

Is this expected? The postfix notation I define seems innocuous, but it actually seems to break tactic parsing. Is it a problem of priority?

```
Require Import Ltac2.Ltac2.
Require Import Ltac2.Message.
Ltac2 print_goal2 () :=
multi_match! goal with
| [ h: _ |- _] => let h := Control.hyp h in print (of_constr h); fail
| [ |- ?g ] => print (of_string "======"); print (of_constr g); ()
end.
Goal forall n m:nat, n<m -> True.
Proof.
intros n m H.
print_goal2(). (* Works OK *)
Ltac2 Notation x(constr) "::" := print (of_constr x).
print_goal2(). (* Error: Syntax error: '::' expected after [constr] (in [ltac2_expr]). *)
```

There have been recent fixes to this. E.g. these notations (https://github.com/coq/coq/blob/f0570d9e5a5ae7107c566d6f05ee9dd9df6b8f3c/user-contrib/Ltac2/Bool.v#L69) don't work in 8.13.

OK thanks.

Last updated: Jun 13 2024 at 04:03 UTC