From 601fd9343a241706c0a205aaf8e08255753c3780 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 29 Sep 2016 15:23:07 +0200 Subject: Arguments: cleanup + detect discrepancy rename/implicit (#3753) It seems warnings are not taken into account in output/ tests. --- test-suite/output/Arguments_renaming.out | 20 +++++++++++++++++--- 1 file changed, 17 insertions(+), 3 deletions(-) (limited to 'test-suite/output/Arguments_renaming.out') diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 3488cb305..815305581 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -1,9 +1,20 @@ +File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 1, characters 0-36: +Warning: Ignoring rename of x into y. Only implicit arguments can be renamed. +[arguments-assert,vernacular] The command has indeed failed with message: Error: To rename arguments the "rename" flag must be specified. Argument A renamed to B. -The command has indeed failed with message: -Error: To rename arguments the "rename" flag must be specified. -Argument A renamed to T. +File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 2, characters 0-25: +Warning: Ignoring rename of A into T. Only implicit arguments can be renamed. +[arguments-assert,vernacular] +File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 2, characters 0-25: +Warning: This command is just asserting the number and 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] +File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 4, characters 0-40: +Warning: Ignoring rename of x into y. Only implicit arguments can be renamed. +[arguments-assert,vernacular] @eq_refl : forall (B : Type) (y : B), y = y eq_refl @@ -110,6 +121,9 @@ The command has indeed failed with message: Error: Argument z cannot be declared implicit. The command has indeed failed with message: Error: Extra argument y. +File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 53, characters 0-26: +Warning: Ignoring rename of x into s. Only implicit arguments can be renamed. +[arguments-assert,vernacular] The command has indeed failed with message: Error: To rename arguments the "rename" flag must be specified. Argument A renamed to R. -- cgit v1.2.3