aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/language
diff options
context:
space:
mode:
Diffstat (limited to 'doc/sphinx/language')
-rw-r--r--doc/sphinx/language/extensions/implicit-arguments.rst2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/language/extensions/implicit-arguments.rst b/doc/sphinx/language/extensions/implicit-arguments.rst
index ca69072cb9..f8375e93ce 100644
--- a/doc/sphinx/language/extensions/implicit-arguments.rst
+++ b/doc/sphinx/language/extensions/implicit-arguments.rst
@@ -217,7 +217,7 @@ usual implicit arguments disambiguation syntax.
The syntax is also supported in internal binders. For instance, in the
following kinds of expressions, the type of each declaration present
-in :token:`binders` can be bracketed to mark the declaration as
+in :n:`{* @binder }` can be bracketed to mark the declaration as
implicit:
* :n:`fun (@ident:forall {* @binder }, @type) => @term`,
* :n:`forall (@ident:forall {* @binder }, @type), @type`,