From 90285ff50290a49d20d60ffc59725bf87c6acd14 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Fri, 1 May 2020 13:22:42 +0200
Subject: Move essential vocabulary and syntax conventions to section on
 basics.

---
 doc/sphinx/user-extensions/syntax-extensions.rst | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

(limited to 'doc/sphinx/user-extensions')

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 93d2439412..d72409e0d9 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1,4 +1,4 @@
-.. _syntaxextensionsandnotationscopes:
+.. _syntax-extensions-and-notation-scopes:
 
 Syntax extensions and notation scopes
 =====================================
@@ -433,9 +433,7 @@ Displaying information about notations
        [ IDENT "try"; SELF
 
    Note that the productions printed by this command are represented in the form used by
-   |Coq|'s parser (coqpp), which differs from how productions are shown in the documentation.  The grammar
-   described in this documentation is equivalent to the grammar of the |Coq| parser, but has been
-   heavily edited to improve readability and presentation.
+   |Coq|'s parser (coqpp), which differs from how productions are shown in the documentation.
 
 .. _locating-notations:
 
@@ -1088,12 +1086,17 @@ ways to change the interpretation of subterms are available.
 Opening a notation scope locally
 ++++++++++++++++++++++++++++++++
 
+.. insertprodn term_scope term_scope
+
+.. prodn::
+   term_scope ::= @term0 % @scope_key
+
 The notation scope stack can be locally extended within
 a :token:`term` with the syntax
-:n:`(@term)%@scope_key` (or simply :n:`@term%@scope_key` for atomic terms).
+:n:`(@term)%@scope_key` (or simply :n:`@term0%@scope_key` for atomic terms).
 
 In this case, :n:`@term` is
-interpreted in the scope stack extended with the scope bound to :token:`ident`.
+interpreted in the scope stack extended with the scope bound to :n:`@scope_key`.
 
 .. cmd:: Delimit Scope @scope_name with @scope_key
 
-- 
cgit v1.2.3