diff options
| author | coqbot-app[bot] | 2020-11-03 23:48:26 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-03 23:48:26 +0000 |
| commit | 5a25287987b8683ee3cbaa9a87ba0f8aebba896b (patch) | |
| tree | dce1ab90cc6785e29848e43deaea6c24b4138866 | |
| parent | 077d479113c6a53543d53514470be3570c89cc8d (diff) | |
| parent | 87be983b7623126320dc0b43303a48ea41b86f5c (diff) | |
Merge PR #13293: Doc: added "Arguments" removing implicit arguments
Reviewed-by: jfehrle
Reviewed-by: Zimmi48
| -rw-r--r-- | doc/sphinx/language/extensions/arguments-command.rst | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/sphinx/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst index 29877e1b32..f8c0e23696 100644 --- a/doc/sphinx/language/extensions/arguments-command.rst +++ b/doc/sphinx/language/extensions/arguments-command.rst @@ -86,6 +86,7 @@ Setting properties of a function's arguments the parameter name used in the function definition). Unless `rename` is specified, the list of :n:`@name`\s must be a prefix of the formal parameters, including all implicit arguments. `_` can be used to skip over a formal parameter. + The construct :n:`@name {? % @scope }` declares :n:`@name` as non-implicit if `clear implicits` is specified or at least one other name is declared implicit in the same list of :n:`@name`\s. :token:`scope` can be either a scope name or its delimiting key. See :ref:`binding_to_scope`. `clear implicits` |