diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-09-29 15:23:07 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-09-29 17:51:06 +0200 |
| commit | 601fd9343a241706c0a205aaf8e08255753c3780 (patch) | |
| tree | 8e704db53a79b588303cd5fe98448e598dd79518 /test-suite/output/Arguments_renaming.out | |
| parent | fdfcdc79989c46737089e4c8cab5ad0090e4d8a6 (diff) | |
Arguments: cleanup + detect discrepancy rename/implicit (#3753)
It seems warnings are not taken into account in output/
tests.
Diffstat (limited to 'test-suite/output/Arguments_renaming.out')
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 20 |
1 files changed, 17 insertions, 3 deletions
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. |