From 775b8f28562d1d5063da2b28a06e59610b76f06f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 30 Sep 2016 10:14:10 +0200 Subject: Ignore file names in warning emitted by test-suite/output/* (#5111) --- test-suite/output/Arguments_renaming.out | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 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 815305581..1633ad976 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -1,20 +1,20 @@ -File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 1, characters 0-36: +File "stdin", line 1, characters 0-36: Warning: Ignoring rename of x into y. Only implicit arguments can be renamed. -[arguments-assert,vernacular] +[arguments-ignore-rename-nonimpl,vernacular] The command has indeed failed with message: Error: To rename arguments the "rename" flag must be specified. Argument A renamed to B. -File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 2, characters 0-25: +File "stdin", 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: +[arguments-ignore-rename-nonimpl,vernacular] +File "stdin", 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: +File "stdin", line 4, characters 0-40: Warning: Ignoring rename of x into y. Only implicit arguments can be renamed. -[arguments-assert,vernacular] +[arguments-ignore-rename-nonimpl,vernacular] @eq_refl : forall (B : Type) (y : B), y = y eq_refl @@ -121,9 +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: +File "stdin", line 53, characters 0-26: Warning: Ignoring rename of x into s. Only implicit arguments can be renamed. -[arguments-assert,vernacular] +[arguments-ignore-rename-nonimpl,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