Add syntax for non maximally inserted implicit arguments

1 files changed, 12 insertions, 0 deletions

diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v
index b16e4a1186..ebbd783dc4 100644
--- a/test-suite/success/ImplicitArguments.v
+++ b/test-suite/success/ImplicitArguments.v
@@ -1,3 +1,15 @@
+
+Axiom foo : forall (x y z t : nat), nat.
+
+Arguments foo {_} _ [z] t.
+Check (foo 1).
+Arguments foo {_} _ {z} {t}.
+Fail Arguments foo {_} _ [z] {t}.
+Check (foo 1).
+
+Definition foo1 [m] n := n + m.
+Check (foo1 1).
+
 Inductive vector {A : Type} : nat -> Type :=
 | vnil : vector 0
 | vcons : A -> forall {n'}, vector n' -> vector (S n').