Fix test-suite fo non maximal implicit arguments

6 files changed, 9 insertions, 9 deletions

diff --git a/test-suite/bugs/closed/bug_2729.v b/test-suite/bugs/closed/bug_2729.v
index ff08bdc6bb..52cc34beb3 100644
--- a/test-suite/bugs/closed/bug_2729.v
+++ b/test-suite/bugs/closed/bug_2729.v
@@ -82,7 +82,7 @@ Inductive SequenceBase (pu : PatchUniverse)
                      (p : pu_type from mid)
                      (qs : SequenceBase pu mid to),
               SequenceBase pu from to.
-Arguments Nil [pu cxt].
+Arguments Nil {pu cxt}.
 Arguments Cons [pu from mid to].
 
 Program Fixpoint insertBase {pu : PatchUniverse}
diff --git a/test-suite/complexity/injection.v b/test-suite/complexity/injection.v
index 298a07c1c4..7022987096 100644
--- a/test-suite/complexity/injection.v
+++ b/test-suite/complexity/injection.v
@@ -47,7 +47,7 @@ Parameter mkJoinmap :   forall (key: Type) (t: Type) (j: joinable t),
 joinmap key j.
 
 Parameter ADMIT: forall p: Prop, p.
-Arguments ADMIT [p].
+Arguments ADMIT {p}.
 
 Module Share.
 Parameter jb : joinable bool.
diff --git a/test-suite/prerequisite/ssr_mini_mathcomp.v b/test-suite/prerequisite/ssr_mini_mathcomp.v
index d293dc0533..048fb3b027 100644
--- a/test-suite/prerequisite/ssr_mini_mathcomp.v
+++ b/test-suite/prerequisite/ssr_mini_mathcomp.v
@@ -65,7 +65,7 @@ Proof. by []. Qed.
 
 Lemma eqP T : Equality.axiom (@eq_op T).
 Proof. by case: T => ? []. Qed.
-Arguments eqP [T x y].
+Arguments eqP {T x y}.
 
 Delimit Scope eq_scope with EQ.
 Open Scope eq_scope.
@@ -345,7 +345,7 @@ Proof. by []. Qed.
 
 End SubEqType.
 
-Arguments val_eqP [T P sT x y].
+Arguments val_eqP {T P sT x y}.
 Prenex Implicits val_eqP.
 
 Notation "[ 'eqMixin' 'of' T 'by' <: ]" := (SubEqMixin _ : Equality.class_of T)
@@ -386,7 +386,7 @@ Qed.
 Canonical nat_eqMixin := EqMixin eqnP.
 Canonical nat_eqType := Eval hnf in EqType nat nat_eqMixin.
 
-Arguments eqnP [x y].
+Arguments eqnP {x y}.
 Prenex Implicits eqnP.
 
 Coercion nat_of_bool (b : bool) := if b then 1 else 0.
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index c2130995fc..804f79c289 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -71,7 +71,7 @@ CoInductive LList (A : Set) : Set :=
   | LNil : LList A
   | LCons : A -> LList A -> LList A.
 
-Arguments LNil [A].
+Arguments LNil {A}.
 
 Inductive Finite (A : Set) : LList A -> Prop :=
   | Finite_LNil : Finite LNil
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v
index 1dbeaf3e1f..8297f54641 100644
--- a/test-suite/success/Inversion.v
+++ b/test-suite/success/Inversion.v
@@ -31,7 +31,7 @@ Inductive in_extension (I : Set) (r : rule I) : extension I -> Type :=
   | in_first : forall e, in_extension r (add_rule r e)
   | in_rest : forall e r', in_extension r e -> in_extension r (add_rule r' e).
 
-Arguments NL [I].
+Arguments NL {I}.
 
 Inductive super_extension (I : Set) (e : extension I) :
 extension I -> Type :=
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index 4fac798f76..15672eab7c 100644
--- a/test-suite/success/RecTutorial.v
+++ b/test-suite/success/RecTutorial.v
@@ -994,7 +994,7 @@ Qed.
 
 
 Arguments Vector.cons [A] _ [n].
-Arguments Vector.nil [A].
+Arguments Vector.nil {A}.
 Arguments Vector.hd [A n].
 Arguments Vector.tl [A n].
 
@@ -1161,7 +1161,7 @@ infiniteproof map_iterate'.
 Qed.
 
 
-Arguments LNil [A].
+Arguments LNil {A}.
 
 Lemma Lnil_not_Lcons : forall (A:Set)(a:A)(l:LList A),
                                LNil <> (LCons a l).