diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-17 22:59:29 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-17 22:59:29 +0000 |
| commit | 961b5160dc4872c60a9adfa7abe9efd5cb140690 (patch) | |
| tree | 4aa97aa70a5c528e0e2106205ddf0723b9291781 /test-suite | |
| parent | 226eb53b43da597c237f8069ebb6c189ba06584c (diff) | |
Command Arguments: standardizing format of error messages and American spelling.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14810 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 925ff693a..5de4ffd16 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -1,5 +1,5 @@ The command has indeed failed with message: -=> Error: to rename arguments the "rename" flag must be specified +=> Error: To rename arguments the "rename" flag must be specified. @eq_refl : forall (B : Type) (y : B), y = y eq_refl @@ -95,12 +95,12 @@ Expands to: Constant Top.myplus myplus : forall Z : Type, Z -> nat -> nat -> nat The command has indeed failed with message: -=> Error: All arguments lists must declare the same names +=> Error: All arguments lists must declare the same names. The command has indeed failed with message: -=> Error: The following arguments are not declared: x +=> Error: The following arguments are not declared: x. The command has indeed failed with message: -=> Error: Arguments names must be distinct +=> Error: Arguments names must be distinct. The command has indeed failed with message: -=> Error: Argument z cannot be declared implicit +=> Error: Argument z cannot be declared implicit. The command has indeed failed with message: -=> Error: Extra argument y +=> Error: Extra argument y. |