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 | |
| 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')
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 4 | ||||
| -rw-r--r-- | test-suite/output/Arguments_renaming.v | 3 | ||||
| -rw-r--r-- | test-suite/success/implicit.v | 13 |
3 files changed, 16 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. - diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index 668d765d83..59650d6822 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -169,3 +169,16 @@ Variable eq0le0' : forall (n : nat) {x : n = 0}, n <= 0. Axiom eq0le0'' : forall (n : nat) {x : n = 0}, n <= 0. Definition eq0le0''' : forall (n : nat) {x : n = 0}, n <= 0. Admitted. Fail Axiom eq0le0'''' : forall [n : nat] {x : n = 0}, n <= 0. + +Module TestUnnamedImplicit. + +Axiom foo : forall A, A -> A. + +Arguments foo {A} {_}. +Check foo (arg_2:=true) : bool. +Check foo : bool. + +Arguments foo {A} {x}. +Check foo (x:=true) : bool. + +End TestUnnamedImplicit. |