Add syntax for non maximally inserted implicit arguments

3 files changed, 25 insertions, 0 deletions

diff --git a/test-suite/success/Generalization.v b/test-suite/success/Generalization.v
index de34e007d2..df729588f4 100644
--- a/test-suite/success/Generalization.v
+++ b/test-suite/success/Generalization.v
@@ -11,4 +11,10 @@ Admitted.
 Print a_eq_b.
 
 
+Require Import Morphisms.
 
+Class Equiv A := equiv : A -> A -> Prop.
+Class Setoid A `{Equiv A} := setoid_equiv:> Equivalence (equiv).
+
+Lemma vcons_proper A `[Equiv A] `[!Setoid A] (x : True) : True.
+Admitted.
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').
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index ecaaedca53..6e12733999 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -157,3 +157,10 @@ Check fun f : forall {_:nat}, nat => f (arg_1:=0).
 Set Warnings "+syntax".
 Check id (fun x => let f c {a} (b:a=a) := b in f true (eq_refl 0)).
 Set Warnings "syntax".
+
+
+Axiom eq0le0 : forall (n : nat) (x : n = 0), n <= 0.
+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.