diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2016-10-28 09:29:25 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2016-10-28 09:29:25 +0200 |
commit | 4f65c0370c5fc4163fa961a7fabb8e90fa7c45dd (patch) | |
tree | 24a84ecb587edb6e14a1e1469f604239b7a6d6c2 /test-suite/output | |
parent | d500a684be14b0c781ea4cda0ee02d3c5cdcad81 (diff) | |
parent | ebb5bd7c2048daa7241bb07d8b53d07e0be27e62 (diff) |
Merge remote-tracking branch 'github/pr/337' into v8.6
Was PR#337: Fix arguments
Diffstat (limited to 'test-suite/output')
-rw-r--r-- | test-suite/output/Arguments.out | 2 | ||||
-rw-r--r-- | test-suite/output/Arguments_renaming.out | 32 | ||||
-rw-r--r-- | test-suite/output/Arguments_renaming.v | 6 |
3 files changed, 15 insertions, 25 deletions
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index 2c7b04c62..a2ee2d4c8 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -101,4 +101,4 @@ Error: Unknown interpretation for notation "$". w 3 true = tt : Prop The command has indeed failed with message: -Error: Extra argument _. +Error: Extra arguments: _, _. diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 1633ad976..9d90de47c 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -1,20 +1,12 @@ -File "stdin", line 1, characters 0-36: -Warning: Ignoring rename of x into y. Only implicit arguments can be renamed. -[arguments-ignore-rename-nonimpl,vernacular] The command has indeed failed with message: -Error: To rename arguments the "rename" flag must be specified. +Error: To rename arguments the "rename" flag must be +specified. Argument A renamed to B. File "stdin", line 2, characters 0-25: -Warning: Ignoring rename of A into T. Only implicit arguments can be renamed. -[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 "stdin", line 4, characters 0-40: -Warning: Ignoring rename of x into y. Only implicit arguments can be renamed. -[arguments-ignore-rename-nonimpl,vernacular] +Warning: This command is just asserting the 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] @eq_refl : forall (B : Type) (y : B), y = y eq_refl @@ -112,18 +104,16 @@ Expands to: Constant Top.myplus @myplus : forall Z : Type, Z -> nat -> nat -> nat The command has indeed failed with message: -Error: All arguments lists must declare the same names. +Error: Arguments lists should agree on names they provide. The command has indeed failed with message: -Error: The following arguments are not declared: x. +Error: Sequences of implicit arguments must be of different lengths. The command has indeed failed with message: Error: Arguments names must be distinct. 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 "stdin", line 53, characters 0-26: -Warning: Ignoring rename of x into s. Only implicit arguments can be renamed. -[arguments-ignore-rename-nonimpl,vernacular] +Error: Extra arguments: y. The command has indeed failed with message: -Error: To rename arguments the "rename" flag must be specified. +Error: To rename arguments the "rename" flag must be +specified. Argument A renamed to R. diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v index e42c98336..2d14c94ac 100644 --- a/test-suite/output/Arguments_renaming.v +++ b/test-suite/output/Arguments_renaming.v @@ -1,5 +1,5 @@ Fail Arguments eq_refl {B y}, [B] y. -Arguments identity T _ _. +Arguments identity A _ _. Arguments eq_refl A x : assert. Arguments eq_refl {B y}, [B] y : rename. @@ -46,9 +46,9 @@ About myplus. Check @myplus. Fail Arguments eq_refl {F g}, [H] k. -Fail Arguments eq_refl {F}, [F]. +Fail Arguments eq_refl {F}, [F] : rename. Fail Arguments eq_refl {F F}, [F] F. -Fail Arguments eq {F} x [z]. +Fail Arguments eq {F} x [z] : rename. Fail Arguments eq {F} x z y. Fail Arguments eq {R} s t. |