aboutsummaryrefslogtreecommitdiff
path: root/vernac/comArguments.ml
diff options
context:
space:
mode:
authorJim Fehrle2020-04-15 11:37:29 -0700
committerJim Fehrle2020-04-15 11:37:29 -0700
commitae84c97ef9b55eca393270325024121102f5c482 (patch)
tree30b360136cbdbc9cfef85d72e6965e6b5db50815 /vernac/comArguments.ml
parente75ad2a575bc73febbf7eb075545e95d102f7544 (diff)
Add needed commas in message
Diffstat (limited to 'vernac/comArguments.ml')
-rw-r--r--vernac/comArguments.ml6
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,