diff options
| author | Guillaume Melquiond | 2015-01-29 13:26:12 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-01-29 13:33:17 +0100 |
| commit | 7b0875326f03dcda8a39cd1920ae712c0dfb9a4b (patch) | |
| tree | f3dac4e8c05c43156f8e2e7f4eecec7d7911ca33 | |
| parent | 3dff646f68c045dbad71d545353e388461fbd909 (diff) | |
Prevent spurious warnings about Arguments.
The Arguments command tends to emit the following warning even when
properly used:
This command is just asserting the number and names of arguments of cons.
If this is what you want add ': assert' to silence the warning. If you
want to clear implicit arguments add ': clear implicits'. If you want to
clear notation scopes add ': clear scopes'
In fact, even ': assert' does not silence it, contrarily to what the message
suggests.
| -rw-r--r-- | toplevel/vernacentries.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index bb20730015..c6e40725ba 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1124,6 +1124,7 @@ let vernac_declare_arguments locality r l nargs flags = vernac_declare_implicits locality r implicits; if nargs >= 0 && nargs < List.fold_left max 0 rargs then error "The \"/\" option must be placed after the last \"!\"."; + let no_flags = List.is_empty flags in let rec narrow = function | #Reductionops.ReductionBehaviour.flag as x :: tl -> x :: narrow tl | [] -> [] | _ :: tl -> narrow tl in @@ -1141,7 +1142,7 @@ let vernac_declare_arguments locality r l nargs flags = some_implicits_specified || some_scopes_specified || some_simpl_flags_specified) && - List.length flags = 0 then + no_flags then msg_warning (strbrk "This command is just asserting the number and names of arguments of " ++ pr_global sr ++ strbrk". If this is what you want add ': assert' to silence the warning. If you want to clear implicit arguments add ': clear implicits'. If you want to clear notation scopes add ': clear scopes'") |