12 files changed, 24 insertions, 24 deletions
diff --git a/test-suite/success/AdvancedTypeClasses.v b/test-suite/success/AdvancedTypeClasses.v
index b4efa7edc..d0aa5c857 100644
--- a/test-suite/success/AdvancedTypeClasses.v
+++ b/test-suite/success/AdvancedTypeClasses.v
@@ -28,8 +28,8 @@ Class interp_pair (abs : Type) :=
  { repr : term;
   link: abs = interp repr }.
 
-Implicit Arguments repr [[interp_pair]].
-Implicit Arguments link [[interp_pair]].
+Arguments repr _ {interp_pair}.
+Arguments link _ {interp_pair}.
 
 Lemma prod_interp `{interp_pair a, interp_pair b} : a * b = interp (Prod (repr a) (repr b)).
   simpl. intros. rewrite <- link. rewrite <- (link b). reflexivity.
diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v
index 921433cad..9a19b595e 100644
--- a/test-suite/success/ImplicitArguments.v
+++ b/test-suite/success/ImplicitArguments.v
@@ -2,7 +2,7 @@ Inductive vector {A : Type} : nat -> Type :=
 | vnil : vector 0
 | vcons : A -> forall {n'}, vector n' -> vector (S n').
 
-Implicit Arguments vector [].
+Arguments vector A : clear implicits.
 
 Require Import Coq.Program.Program.
 
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index 5b1482fd5..f07c0191f 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -73,7 +73,7 @@ CoInductive LList (A : Set) : Set :=
   | LNil : LList A
   | LCons : A -> LList A -> LList A.
 
-Implicit 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 45c71615f..ca8da3948 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).
 
-Implicit 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 841940492..29350d620 100644
--- a/test-suite/success/RecTutorial.v
+++ b/test-suite/success/RecTutorial.v
@@ -991,10 +991,10 @@ Proof.
 Qed.
 
 
-Implicit Arguments Vector.cons [A n].
-Implicit Arguments Vector.nil [A].
-Implicit Arguments Vector.hd [A n].
-Implicit Arguments Vector.tl [A n].
+Arguments Vector.cons [A] _ [n].
+Arguments Vector.nil [A].
+Arguments Vector.hd [A n].
+Arguments Vector.tl [A n].
 
 Definition Vid : forall (A : Type)(n:nat), Vector.t A n -> Vector.t A n.
 Proof.
@@ -1064,7 +1064,7 @@ Fixpoint vector_nth (A:Set)(n:nat)(p:nat)(v:Vector.t A p){struct v}
   | S n', Vector.cons _ v' => vector_nth A n' _ v'
   end.
 
-Implicit Arguments vector_nth [A p].
+Arguments vector_nth [A] _ [p].
 
 
 Lemma nth_bitwise : forall (n:nat) (v1 v2: Vector.t bool n) i  a b,
@@ -1159,7 +1159,7 @@ infiniteproof map_iterate'.
 Qed.
 
 
-Implicit Arguments LNil [A].
+Arguments LNil [A].
 
 Lemma Lnil_not_Lcons : forall (A:Set)(a:A)(l:LList A),
                                LNil <> (LCons a l).
diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v
index 6f27c1d36..18ebcd638 100644
--- a/test-suite/success/Record.v
+++ b/test-suite/success/Record.v
@@ -5,7 +5,7 @@ Require Import Program.
 Require Import List.
 
 Record vector {A : Type} {n : nat} := { vec_list : list A ; vec_len : length vec_list = n }.
-Implicit Arguments vector [].
+Arguments vector : clear implicits.
 
 Coercion vec_list : vector >-> list.
 
diff --git a/test-suite/success/Scopes.v b/test-suite/success/Scopes.v
index ca3746716..2da630633 100644
--- a/test-suite/success/Scopes.v
+++ b/test-suite/success/Scopes.v
@@ -11,7 +11,7 @@ Check (A.opp 3).
 
 Record B := { f :> Z -> Z }.
 Variable a:B.
-Arguments Scope a [Z_scope].
+Arguments a _%Z_scope : extra scopes.
 Check a 0.
 
 (* Check that casts activate scopes if ever possible *)
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index cd6eac35c..400479ae8 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -128,8 +128,8 @@ Record Monad {m : Type -> Type} := {
 
 Print Visibility.
 Print unit.
-Implicit Arguments unit [[m] [m0] [α]].
-Implicit Arguments Monad [].
+Arguments unit {m m0 α}.
+Arguments Monad : clear implicits.
 Notation "'return' t" := (unit t).
 
 (* Test correct handling of existentials and defined fields. *)
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 02e043bc3..b287b5fac 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -39,7 +39,7 @@ Qed.
 (* Check apply/eapply distinction in presence of open terms *)
 
 Parameter h : forall x y z : nat, x = z -> x = y.
-Implicit Arguments h [[x] [y]].
+Arguments h {x y}.
 Goal 1 = 0 -> True.
 intro H.
 apply h in H || exact I.
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index f5bb884d2..55ae54ca0 100644
--- a/test-suite/success/dependentind.v
+++ b/test-suite/success/dependentind.v
@@ -42,7 +42,7 @@ Inductive ctx : Type :=
 Bind Scope context_scope with ctx.
 Delimit Scope context_scope with ctx.
 
-Arguments Scope snoc [context_scope].
+Arguments snoc _%context_scope.
 
 Notation " Γ , τ " := (snoc Γ τ) (at level 25, τ at next level, left associativity) : context_scope.
 
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 627794832..5b13f35d5 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -386,7 +386,7 @@ Record iffT (X Y:Type) : Type := mkIff { iffLR : X->Y; iffRL : Y->X }.
 Record tri (R:Type->Type->Type) (S:Type->Type->Type) (T:Type->Type->Type) := mkTri {
   tri0 : forall a b c, R a b -> S a c -> T b c
 }.
-Implicit Arguments mkTri [R S T].
+Arguments mkTri [R S T].
 Definition tri_iffT : tri iffT iffT iffT :=
   (mkTri
     (fun X0 X1 X2 E01 E02 =>
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index a0981311b..23853890d 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -33,11 +33,11 @@ Definition eq1 := fun (A:Type) (x y:A) => x=y.
 Definition eq2 := fun (A:Type) (x y:A) => x=y.
 Definition eq3 := fun (A:Type) (x y:A) => x=y.
 
-Implicit Arguments op' [].
-Global Implicit Arguments op'' [].
+Arguments op' : clear implicits.
+Global Arguments op'' : clear implicits.
 
-Implicit Arguments eq2 [].
-Global Implicit Arguments eq3 [].
+Arguments eq2 : clear implicits.
+Global Arguments eq3 : clear implicits.
 
 Check (op 0 0).
 Check (op' nat 0 0).
@@ -89,14 +89,14 @@ Fixpoint plus n m {struct n} :=
 
 (* Check multiple implicit arguments signatures *)
 
-Implicit Arguments eq_refl [[A] [x]] [[A]].
+Arguments eq_refl {A x}, {A}.
 
 Check eq_refl : 0 = 0.
 
 (* Check that notations preserve implicit (since 8.3) *)
 
 Parameter p : forall A, A -> forall n, n = 0 -> True.
-Implicit Arguments p [A n].
+Arguments p [A] _ [n].
 Notation Q := (p 0).
 Check Q eq_refl.