From d9ab85ffae85e756b2ed94c3b3fe655d3b541aaf Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Tue, 3 Mar 2020 10:23:15 -0800
Subject: Remove some productionlists

---
 doc/sphinx/user-extensions/syntax-extensions.rst | 4 ++--
 1 file changed, 2 insertions(+), 2 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 fd95a5cef4..669975ba7e 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -947,7 +947,7 @@ notations are given below. The optional :production:`scope` is described in
 
 .. prodn::
    decl_notations ::= where @decl_notation {* and @decl_notation }
-   decl_notation ::= @string := @term1_extended [(only parsing)] {? : @ident }
+   decl_notation ::= @string := @one_term {? ( only parsing ) } {? : @ident }
 
 .. note:: No typing of the denoted expression is performed at definition
           time. Type checking is done only at the time of use of the notation.
@@ -1194,7 +1194,7 @@ Binding arguments of a constant to an interpretation scope
 Binding types of arguments to an interpretation scope
 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 
-.. cmd:: Bind Scope @scope with @qualid
+.. cmd:: Bind Scope @ident with {+ @class }
 
    When an interpretation scope is naturally associated to a type (e.g.  the
    scope of operations on the natural numbers), it may be convenient to bind it
-- 
cgit v1.2.3