From ae84c97ef9b55eca393270325024121102f5c482 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Wed, 15 Apr 2020 11:37:29 -0700
Subject: Add needed commas in message

---
 test-suite/output/Arguments_renaming.out | 6 +++---
 vernac/comArguments.ml                   | 6 +++---
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index abc7f0f88e..e0aa758812 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -2,9 +2,9 @@ The command has indeed failed with message:
 Flag "rename" expected to rename A into B.
 File "stdin", line 3, characters 0-25:
 Warning: This command is just asserting the names of arguments of identity.
-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' [arguments-assert,vernacular]
+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' [arguments-assert,vernacular]
 @eq_refl
      : forall (B : Type) (y : B), y = y
 eq_refl
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,
-- 
cgit v1.2.3