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.
Last updated: Dec 07 2023 at 06:38 UTC