diff options
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/implicit.v | 13 |
1 files changed, 13 insertions, 0 deletions
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. |