@Pierre-Marie Pédrot , what's the top-level Entry.t for Ltac2 where the Ltac2 Notation rules are added?
Entry.t
Ltac2 Notation
I want to write a Print Ltac2 Grammar actually
Print Ltac2 Grammar
Last updated: Oct 08 2024 at 15:02 UTC