From 45e064836ec1f50300198f89c099b71d0e2059b9 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 8 Apr 2021 14:33:15 +0200 Subject: Register Ltac2 grammar entry as "ltac2" for the Print Grammar vernacular. Fixes #14092: Print Grammar ltac2 should exist. --- doc/changelog/07-vernac-commands-and-options/14093-fix-14092.rst | 6 ++++++ doc/sphinx/user-extensions/syntax-extensions.rst | 1 + user-contrib/Ltac2/tac2entries.ml | 6 ++++++ 3 files changed, 13 insertions(+) create mode 100644 doc/changelog/07-vernac-commands-and-options/14093-fix-14092.rst diff --git a/doc/changelog/07-vernac-commands-and-options/14093-fix-14092.rst b/doc/changelog/07-vernac-commands-and-options/14093-fix-14092.rst new file mode 100644 index 0000000000..7831d10392 --- /dev/null +++ b/doc/changelog/07-vernac-commands-and-options/14093-fix-14092.rst @@ -0,0 +1,6 @@ +- **Added:** + The Ltac2 grammar can now be printed using the + Print Grammar ltac2 command + (`#14093 `_, + fixes `#14092 `_, + by Pierre-Marie Pédrot). diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 453e878a5d..d212256765 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -467,6 +467,7 @@ Displaying information about notations - `tactic` - for currently-defined tactic notations, :token:`tactic`\s and tacticals (corresponding to :token:`ltac_expr` in the documentation). - `vernac` - for :token:`command`\s + - `ltac2` - for Ltac2 notations (corresponding to :token:`ltac2_expr`) This command doesn't display all nonterminals of the grammar. For example, productions shown by `Print Grammar tactic` refer to nonterminals `tactic_then_locality` diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index 6be5ba80d5..7af530ab0f 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -50,6 +50,12 @@ let q_pose = Pcoq.Entry.create "q_pose" let q_assert = Pcoq.Entry.create "q_assert" end +let () = + let entries = [ + Pcoq.AnyEntry Pltac.ltac2_expr; + ] in + Pcoq.register_grammars_by_name "ltac2" entries + (** Tactic definition *) type tacdef = { -- cgit v1.2.3