Merge PR #11961: Convert vernac commands chapter to prodn, update syntax

Ack-by: Zimmi48
Ack-by: cpitclaudel

1 files changed, 5 insertions, 5 deletions

diff --git a/doc/sphinx/language/extensions/implicit-arguments.rst b/doc/sphinx/language/extensions/implicit-arguments.rst
index fb762a00f1..36ce2fdd25 100644
--- a/doc/sphinx/language/extensions/implicit-arguments.rst
+++ b/doc/sphinx/language/extensions/implicit-arguments.rst
@@ -273,14 +273,14 @@ Declaring Implicit Arguments
    .. prodn::
       smart_qualid ::= @qualid
       | @by_notation
-      by_notation ::= @string {? % @ident }
+      by_notation ::= @string {? % @scope }
       argument_spec_block ::= @argument_spec
       | /
       | &
-      | ( {+ @argument_spec } ) {? % @ident }
-      | [ {+ @argument_spec } ] {? % @ident }
-      | %{ {+ @argument_spec } %} {? % @ident }
-      argument_spec ::= {? ! } @name {? % @ident }
+      | ( {+ @argument_spec } ) {? % @scope }
+      | [ {+ @argument_spec } ] {? % @scope }
+      | %{ {+ @argument_spec } %} {? % @scope }
+      argument_spec ::= {? ! } @name {? % @scope }
       more_implicits_block ::= @name
       | [ {+ @name } ]
       | %{ {+ @name } %}