From 7ff035754c1b728ea0314c60d963ba3505898fe5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 11 Nov 2019 12:03:28 +0100
Subject: Arguments: removing the restriction to set an anonymous parameter
 implicit.

This was already possible manually using "{ _ }" in the type of
declaration. This was also possible for type classes. So, no reason to
forbid in Arguments.
---
 test-suite/success/implicit.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'test-suite/success/implicit.v')

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.
-- 
cgit v1.2.3