Merge PR #11098: Let Arguments support anonymous implicit arguments

Reviewed-by: Zimmi48
Reviewed-by: ejgallego

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.