diff options
| author | Fabian Kunze | 2020-11-27 10:20:40 +0100 |
|---|---|---|
| committer | Fabian Kunze | 2020-11-27 10:20:40 +0100 |
| commit | ce8569a3713536e510381e4d49d534a447cfe637 (patch) | |
| tree | cc56e57ccbbd1c3424ac95bb183466070db746fc | |
| parent | 66429ecca2cc28875ec37b879806744bd3a63179 (diff) | |
Fix #13283: improved error on `clear implicit` flag
| -rw-r--r-- | doc/sphinx/language/extensions/arguments-command.rst | 14 | ||||
| -rw-r--r-- | vernac/comArguments.ml | 4 |
2 files changed, 16 insertions, 2 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` diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml index adf1f42beb..a21af12785 100644 --- a/vernac/comArguments.ml +++ b/vernac/comArguments.ml @@ -223,10 +223,10 @@ let vernac_arguments ~section_local reference args more_implicits flags = | _ -> true in if implicits_specified && clear_implicits_flag then - CErrors.user_err Pp.(str "The \"clear implicits\" flag is incompatible with implicit annotations"); + CErrors.user_err Pp.(str "The \"clear implicits\" flag must be omitted if implicit annotations are given."); if implicits_specified && default_implicits_flag then - CErrors.user_err Pp.(str "The \"default implicits\" flag is incompatible with implicit annotations"); + CErrors.user_err Pp.(str "The \"default implicits\" flag is incompatible with implicit annotations."); let rargs = Util.List.map_filter (function (n, true) -> Some n | _ -> None) |