From 961b5160dc4872c60a9adfa7abe9efd5cb140690 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 17 Dec 2011 22:59:29 +0000 Subject: 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 --- test-suite/output/Arguments_renaming.out | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'test-suite') 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. -- cgit v1.2.3