diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-09-30 10:14:10 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-09-30 10:54:42 +0200 |
| commit | 775b8f28562d1d5063da2b28a06e59610b76f06f (patch) | |
| tree | f8360212d2dabfbae2ebe06aa5d7b40cc3247992 /test-suite/output/Arguments_renaming.out | |
| parent | 61112fa8bd336b17f4a2e724c4751c550f27c69a (diff) | |
Ignore file names in warning emitted by test-suite/output/* (#5111)
Diffstat (limited to 'test-suite/output/Arguments_renaming.out')
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 18 |
1 files changed, 9 insertions, 9 deletions
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. |