diff options
| author | Gaëtan Gilbert | 2020-04-16 16:35:47 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-04-16 16:35:47 +0200 |
| commit | 98eed893760510171e9e8285aac1a8fbeba9afd1 (patch) | |
| tree | b75704ae741ea9a0a4da098ae30c1ab50855e9b3 | |
| parent | 0754dfc001218a8124609418e58896ef18d6b6cf (diff) | |
| parent | ae84c97ef9b55eca393270325024121102f5c482 (diff) | |
Merge PR #12101: Add needed commas in message
Reviewed-by: SkySkimmer
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 6 | ||||
| -rw-r--r-- | 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, |