diff options
Diffstat (limited to 'test-suite/output/Arguments_renaming.out')
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index ed08334e73..925ff693a7 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -1,3 +1,5 @@ +The command has indeed failed with message: +=> Error: to rename arguments the "rename" flag must be specified @eq_refl : forall (B : Type) (y : B), y = y eq_refl @@ -99,6 +101,6 @@ The command has indeed failed with message: The command has indeed failed with message: => Error: Arguments names must be distinct The command has indeed failed with message: -=> Error: Argument z is anonymous and cannot be declared implicit +=> Error: Argument z cannot be declared implicit The command has indeed failed with message: => Error: Extra argument y |