Stream: Ltac2

Topic: Postfix Ltac2 notation

view this post on Zulip Pierre Courtieu (Jun 29 2021 at 07:11):

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]). *)

view this post on Zulip Michael Soegtrop (Jun 29 2021 at 07:22):

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.

view this post on Zulip Pierre Courtieu (Jun 29 2021 at 07:24):

OK thanks.

Last updated: Apr 20 2024 at 04:02 UTC