aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-11-27 17:04:01 +0000
committerGitHub2020-11-27 17:04:01 +0000
commit0501761b95f4fd3e22b93aa6bce8c9f96b88495b (patch)
tree672b5f5916402923ac59329f3f068d7d758ecf19 /doc
parentf733414e59afb37cad41c65b11bc4c817bd137f9 (diff)
parentce8569a3713536e510381e4d49d534a447cfe637 (diff)
Merge PR #13483: Fix #13283: improved error on `clear implicit` flag
Reviewed-by: Zimmi48
Diffstat (limited to 'doc')
-rw-r--r--doc/sphinx/language/extensions/arguments-command.rst14
1 files changed, 14 insertions, 0 deletions
diff --git a/doc/sphinx/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst
index 2460461ede..95c5914e47 100644
--- a/doc/sphinx/language/extensions/arguments-command.rst
+++ b/doc/sphinx/language/extensions/arguments-command.rst
@@ -89,11 +89,25 @@ Setting properties of a function's arguments
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`.
+ .. exn:: To rename arguments the 'rename' flag must be specified.
+ :undocumented:
+
+ .. exn:: Flag 'rename' expected to rename @name into @name.
+ :undocumented:
+
`clear implicits`
makes all implicit arguments into explicit arguments
+
+ .. exn:: The 'clear implicits' flag must be omitted if implicit annotations are given.
+ :undocumented:
+
`default implicits`
automatically determine the implicit arguments of the object.
See :ref:`auto_decl_implicit_args`.
+
+ .. exn:: The 'default implicits' flag is incompatible with implicit annotations.
+ :undocumented:
+
`rename`
rename implicit arguments for the object. See the example :ref:`here <renaming_implicit_arguments>`.
`assert`