diff options
| author | Théo Zimmermann | 2020-09-27 12:31:14 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-09-27 12:31:14 +0200 |
| commit | c571af2f95cccfbffe4e0b93525066676e7f652d (patch) | |
| tree | 68d4f8fd36d03482d2a33ee5e64d5ff813ebbe2c /doc/sphinx/language | |
| parent | 9c2228ff011dc6188b70084fa1e1a5158affcf24 (diff) | |
Reduce nitpick_ignore list a little.
Diffstat (limited to 'doc/sphinx/language')
| -rw-r--r-- | doc/sphinx/language/extensions/implicit-arguments.rst | 2 |
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`, |