From de91dd47e1e4f2366eb4f4cc174aadf8fc2ce1ce Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 11 May 2020 17:41:58 +0200
Subject: Document new Search features.

---
 doc/sphinx/language/extensions/arguments-command.rst | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'doc/sphinx/language')

diff --git a/doc/sphinx/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst
index 34a48b368b..510a97d171 100644
--- a/doc/sphinx/language/extensions/arguments-command.rst
+++ b/doc/sphinx/language/extensions/arguments-command.rst
@@ -6,12 +6,9 @@ Setting properties of a function's arguments
 .. cmd:: Arguments @smart_qualid {* @arg_specs } {* , {* @implicits_alt } } {? : {+, @args_modifier } }
    :name: Arguments
 
-   .. insertprodn smart_qualid args_modifier
+   .. insertprodn argument_spec args_modifier
 
    .. prodn::
-      smart_qualid ::= @qualid
-      | @by_notation
-      by_notation ::= @string {? % @scope_key }
       argument_spec ::= {? ! } @name {? % @scope_key }
       arg_specs ::= @argument_spec
       | /
-- 
cgit v1.2.3