Merge PR #10061: Print custom grammar entries

Reviewed-by: Zimmi48
Ack-by: ejgallego
Ack-by: jashug

2 files changed, 8 insertions, 3 deletions

diff --git a/doc/changelog/03-notations/10061-print-custom-grammar.rst b/doc/changelog/03-notations/10061-print-custom-grammar.rst
new file mode 100644
index 0000000000..8786c7ce6b
--- /dev/null
+++ b/doc/changelog/03-notations/10061-print-custom-grammar.rst
@@ -0,0 +1,4 @@
+- Allow inspecting custom grammar entries by :cmd:`Print Custom Grammar`
+  (`#10061 <https://github.com/coq/coq/pull/10061>`_,
+  fixes `#9681 <http://github.com/coq/coq/pull/9681>`_,
+  by Jasper Hugunin, review by Pierre-Marie Pédrot and Hugo Herbelin).
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index ac079ea7d5..edec13f681 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -840,10 +840,11 @@ gives a way to let any arbitrary expression which is not handled by the
 custom entry ``expr`` be parsed or printed by the main grammar of term
 up to the insertion of a pair of curly brackets.
 
-.. cmd:: Print Grammar @ident.
+.. cmd:: Print Custom Grammar @ident.
+   :name: Print Custom Grammar
 
-   This displays the state of the grammar for terms and grammar for
-   patterns associated to the custom entry :token:`ident`.
+   This displays the state of the grammar for terms associated to
+   the custom entry :token:`ident`.
 
 Summary
 ~~~~~~~