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 /test-suite | |
| parent | 0754dfc001218a8124609418e58896ef18d6b6cf (diff) | |
| parent | ae84c97ef9b55eca393270325024121102f5c482 (diff) | |
Merge PR #12101: Add needed commas in message
Reviewed-by: SkySkimmer
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 6 |
1 files changed, 3 insertions, 3 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 |