diff options
| author | Emilio Jesus Gallego Arias | 2020-02-13 15:35:21 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-13 15:35:21 +0100 |
| commit | eb83c142eb33de18e3bfdd7c32ecfb797a640c38 (patch) | |
| tree | 279ecfcf59459e2601e88e911995d021f88c74b6 /test-suite/output | |
| parent | e76b9da873d2e690e9dd24ed36ecec505676651e (diff) | |
| parent | 7ff035754c1b728ea0314c60d963ba3505898fe5 (diff) | |
Merge PR #11098: Let Arguments support anonymous implicit arguments
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 4 | ||||
| -rw-r--r-- | test-suite/output/Arguments_renaming.v | 3 |
2 files changed, 3 insertions, 4 deletions
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 5093e785de..26ebd8efc3 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -86,8 +86,8 @@ Sequences of implicit arguments must be of different lengths. The command has indeed failed with message: Some argument names are duplicated: F The command has indeed failed with message: -Argument number 2 (anonymous in original definition) cannot be declared -implicit. +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: Extra arguments: y. The command has indeed failed with message: diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v index 9713a9dbbe..6ac09cf771 100644 --- a/test-suite/output/Arguments_renaming.v +++ b/test-suite/output/Arguments_renaming.v @@ -49,7 +49,6 @@ Check @myplus. Fail Arguments eq_refl {F g}, [H] k. Fail Arguments eq_refl {F}, [F] : rename. Fail Arguments eq_refl {F F}, [F] F : rename. -Fail Arguments eq {F} x [z] : rename. +Fail Arguments eq {A} x [z] : rename. Fail Arguments eq {F} x z y. Fail Arguments eq {R} s t. - |