diff options
| author | Jim Fehrle | 2020-04-15 11:37:29 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-04-15 11:37:29 -0700 |
| commit | ae84c97ef9b55eca393270325024121102f5c482 (patch) | |
| tree | 30b360136cbdbc9cfef85d72e6965e6b5db50815 /vernac/comArguments.ml | |
| parent | e75ad2a575bc73febbf7eb075545e95d102f7544 (diff) | |
Add needed commas in message
Diffstat (limited to 'vernac/comArguments.ml')
| -rw-r--r-- | vernac/comArguments.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml index 90791a0906..360e228bfc 100644 --- a/vernac/comArguments.ml +++ b/vernac/comArguments.ml @@ -52,10 +52,10 @@ let warn_arguments_assert = CWarnings.create ~name:"arguments-assert" ~category:"vernacular" Pp.(fun sr -> strbrk "This command is just asserting the names of arguments of " ++ - Printer.pr_global sr ++ strbrk". If this is what you want add " ++ + Printer.pr_global sr ++ strbrk". If this is what you want, add " ++ strbrk "': assert' to silence the warning. If you want " ++ - strbrk "to clear implicit arguments add ': clear implicits'. " ++ - strbrk "If you want to clear notation scopes add ': clear scopes'") + strbrk "to clear implicit arguments, add ': clear implicits'. " ++ + strbrk "If you want to clear notation scopes, add ': clear scopes'") (* [nargs_for_red] is the number of arguments required to trigger reduction, [args] is the main list of arguments statuses, |
