diff options
| author | Hugo Herbelin | 2020-08-22 12:48:07 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-28 15:34:00 +0200 |
| commit | 699eb941cbdd2b3caf98f18b2d49b249b598ca1b (patch) | |
| tree | ad1bc6c93d8d914d09724a19561baa1899d4e7b9 /test-suite | |
| parent | 3df82e1adcfb96320b3fbbb622d9e54cb0a176e1 (diff) | |
When reporting an implicit argument error on a rename argument, use the renaming.
Example:
> Arguments id [B] {b} : rename.
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Argument B is a trailing implicit, so it can't be declared non
maximal. Please use { } instead of [ ].
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 3 | ||||
| -rw-r--r-- | test-suite/output/Arguments_renaming.v | 1 |
2 files changed, 4 insertions, 0 deletions
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 60944759c4..533e64f5b4 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -87,6 +87,9 @@ The command has indeed failed with message: Argument number 3 is a trailing implicit, so it can't be declared non maximal. Please use { } instead of [ ]. The command has indeed failed with message: +Argument z is a trailing implicit, so it can't be declared non maximal. +Please use { } instead of [ ]. +The command has indeed failed with message: Extra arguments: y. The command has indeed failed with message: Flag "rename" expected to rename A into R. diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v index 6001850046..13bda0c070 100644 --- a/test-suite/output/Arguments_renaming.v +++ b/test-suite/output/Arguments_renaming.v @@ -48,6 +48,7 @@ Check @myplus. Fail Arguments eq_refl {F g}, [H] k. Fail Arguments eq_refl {F}, [F] : rename. +Fail Arguments eq {A} x [_] : rename. Fail Arguments eq {A} x [z] : rename. Fail Arguments eq {F} x z y. Fail Arguments eq {R} s t. |