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/sphinx/user-extensions/syntax-extensions.rst | 1 +
 1 file changed, 1 insertion(+)

(limited to 'doc/sphinx')

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`
-- 
cgit v1.2.3