Change Implicit Arguments to Arguments in test-suite

37 files changed, 62 insertions, 63 deletions

diff --git a/test-suite/bugs/closed/1341.v b/test-suite/bugs/closed/1341.v
index 8c5a38859..79a0a14d7 100644
--- a/test-suite/bugs/closed/1341.v
+++ b/test-suite/bugs/closed/1341.v
@@ -8,7 +8,7 @@ Hypothesis Xst : forall A, Equivalence (Xeq A).
 
 Variable map : forall A B, (A -> B) -> X A -> X B.
 
-Implicit Arguments map [A B].
+Arguments map [A B].
 
 Goal forall A B (a b:X (B -> A)) (c:X A) (f:A -> B -> A), Xeq _ a b -> Xeq _ b (map f c) -> Xeq _ a (map f c).
 intros A B a b c f Hab Hbc.
diff --git a/test-suite/bugs/closed/1844.v b/test-suite/bugs/closed/1844.v
index 17eeb3529..c41e45900 100644
--- a/test-suite/bugs/closed/1844.v
+++ b/test-suite/bugs/closed/1844.v
@@ -5,7 +5,7 @@ Definition zeq := Z.eq_dec.
 Definition update (A: Set) (x: Z) (v: A) (s: Z -> A) : Z -> A :=
  fun y => if zeq x y then v else s y.
 
-Implicit Arguments update [A].
+Arguments update [A].
 
 Definition ident := Z.
 Parameter operator: Set.
diff --git a/test-suite/bugs/closed/1891.v b/test-suite/bugs/closed/1891.v
index 685811176..5024a5bc9 100644
--- a/test-suite/bugs/closed/1891.v
+++ b/test-suite/bugs/closed/1891.v
@@ -3,7 +3,7 @@
 
   Definition f (A: Set) (l: T A): unit := tt.
 
-  Implicit Arguments f [A].
+  Arguments f [A].
 
   Lemma L (x: T unit): (unit -> T unit) -> unit.
   Proof.
diff --git a/test-suite/bugs/closed/1951.v b/test-suite/bugs/closed/1951.v
index 7558b0b86..e950554c4 100644
--- a/test-suite/bugs/closed/1951.v
+++ b/test-suite/bugs/closed/1951.v
@@ -42,7 +42,7 @@ match s as a return (S a) with
           pair (ind2 a0) IHl) l)
 end. (* some induction principle *)
 
-Implicit Arguments ind [S].
+Arguments ind [S].
 
 Lemma k : a -> Type. (* some ininteresting lemma *)
 intro;pattern H;apply ind;intros.
diff --git a/test-suite/bugs/closed/1981.v b/test-suite/bugs/closed/1981.v
index 99952682d..a3d942930 100644
--- a/test-suite/bugs/closed/1981.v
+++ b/test-suite/bugs/closed/1981.v
@@ -1,4 +1,4 @@
-Implicit Arguments ex_intro [A].
+Arguments ex_intro [A].
 
 Goal exists n : nat, True.
   eapply ex_intro. exact 0. exact I.
diff --git a/test-suite/bugs/closed/2362.v b/test-suite/bugs/closed/2362.v
index febb9c7bb..10e86cd12 100644
--- a/test-suite/bugs/closed/2362.v
+++ b/test-suite/bugs/closed/2362.v
@@ -8,7 +8,7 @@ Class Pointed (M:Type -> Type) :=
 Unset Implicit Arguments.
 Inductive FPair (A B:Type) (neutral: B) : Type:=
  fpair : forall (a:A) (b:B), FPair A B neutral.
-Implicit Arguments fpair [[A] [B] [neutral]].
+Arguments fpair {A B neutral}.
 
 Set Implicit Arguments.
 
diff --git a/test-suite/bugs/closed/2378.v b/test-suite/bugs/closed/2378.v
index 23a58501f..6d73d58d4 100644
--- a/test-suite/bugs/closed/2378.v
+++ b/test-suite/bugs/closed/2378.v
@@ -63,7 +63,7 @@ Fixpoint lpSat st f: Prop :=
   end.
 End PropLogic.
 
-Implicit Arguments lpSat.
+Arguments lpSat : default implicits.
 
 Fixpoint LPTransfo Pred1 Pred2 p2lp (f: LP Pred1): LP Pred2 :=
   match f with
@@ -71,7 +71,7 @@ Fixpoint LPTransfo Pred1 Pred2 p2lp (f: LP Pred1): LP Pred2 :=
   | LPAnd _ f1 f2 => LPAnd _ (LPTransfo Pred1 Pred2 p2lp f1) (LPTransfo Pred1 Pred2 p2lp f2)
   | LPNot _ f1 => LPNot _ (LPTransfo Pred1 Pred2 p2lp f1)
   end.
-Implicit Arguments LPTransfo.
+Arguments LPTransfo : default implicits.
 
 Definition addIndex (Ind:Type) (Pred: Ind -> Type) (i: Ind) f := 
   LPTransfo (fun p => LPPred _ (existT (fun i => Pred i) i p)) f.
@@ -139,7 +139,7 @@ Definition trProd (State: Type) Ind (Pred: Ind -> Type) (tts: Ind -> TTS State)
   {i:Ind & Pred i} -> LP (Predicate _ (TTSIndexedProduct _ Ind tts)) :=
   fun p => addIndex Ind _ (projS1 p) (tr (projS1 p) (projS2 p)).
 
-Implicit Arguments trProd.
+Arguments trProd : default implicits.
 Require Import Setoid.
 
 Theorem satTrProd:
diff --git a/test-suite/bugs/closed/2404.v b/test-suite/bugs/closed/2404.v
index 8ac696e91..f6ec67601 100644
--- a/test-suite/bugs/closed/2404.v
+++ b/test-suite/bugs/closed/2404.v
@@ -22,13 +22,13 @@ Section Derived.
   Definition bexportw := exportw base.
   Definition bwweak := wweak base.
 
-  Implicit Arguments bexportw [a b].
+  Arguments bexportw [a b].
 
 Inductive RstarSetProof {I : Type} (T : I -> I -> Type) : I -> I -> Type :=
   starReflS : forall a, RstarSetProof T a a
 | starTransS : forall i j k, T i j -> (RstarSetProof T j k) -> RstarSetProof T i k.
 
-Implicit Arguments starTransS [I T i j k].
+Arguments starTransS [I T i j k].
 
 Definition RstarInv {A : Set} (rel : relation A) : A -> A -> Type :=  (flip (RstarSetProof (flip rel))).
 
diff --git a/test-suite/bugs/closed/2584.v b/test-suite/bugs/closed/2584.v
index ef2e4e355..b5a723b47 100644
--- a/test-suite/bugs/closed/2584.v
+++ b/test-suite/bugs/closed/2584.v
@@ -8,7 +8,7 @@ Inductive res (A: Type) : Type :=
 | OK: A -> res A
 | Error: err -> res A. 
 
-Implicit Arguments Error [A].
+Arguments Error [A].
 
 Set Printing Universes.
 
diff --git a/test-suite/bugs/closed/2667.v b/test-suite/bugs/closed/2667.v
index 0631e5358..0e6d0108c 100644
--- a/test-suite/bugs/closed/2667.v
+++ b/test-suite/bugs/closed/2667.v
@@ -1,11 +1,11 @@
-(* Check that extra arguments to Arguments Scope do not disturb use of *)
+(* Check that extra arguments to Arguments do not disturb use of *)
 (* scopes in constructors *)
 
 Inductive stmt : Type := Sskip: stmt | Scall : nat -> stmt.
 Bind Scope Cminor with stmt.
 
 (* extra argument is ok because of possible coercion to funclass *)
-Arguments Scope Scall [_ Cminor ].
+Arguments Scall _ _%Cminor : extra scopes.
 
 (* extra argument is ok because of possible coercion to funclass *)
 Fixpoint f (c: stmt) : Prop := match c with Scall _ => False | _ => False end.
diff --git a/test-suite/bugs/closed/2729.v b/test-suite/bugs/closed/2729.v
index 7929b8810..c9d65c12c 100644
--- a/test-suite/bugs/closed/2729.v
+++ b/test-suite/bugs/closed/2729.v
@@ -82,8 +82,8 @@ Inductive SequenceBase (pu : PatchUniverse)
                      (p : pu_type from mid)
                      (qs : SequenceBase pu mid to),
               SequenceBase pu from to.
-Implicit Arguments Nil [pu cxt].
-Implicit Arguments Cons [pu from mid to].
+Arguments Nil [pu cxt].
+Arguments Cons [pu from mid to].
 
 Program Fixpoint insertBase {pu : PatchUniverse}
                             {from mid to : NameSet}
diff --git a/test-suite/bugs/closed/2830.v b/test-suite/bugs/closed/2830.v
index bb607b785..07a5cf91a 100644
--- a/test-suite/bugs/closed/2830.v
+++ b/test-suite/bugs/closed/2830.v
@@ -49,9 +49,9 @@ Record ageable_facts (A:Type) (level: A -> nat) (age1:A -> option A)  :=
 ; af_level2 : forall x y, age1 x = Some y -> level x = S (level y)
 }.
 
-Implicit Arguments af_unage [[A] [level] [age1]].
-Implicit Arguments af_level1 [[A] [level] [age1]].
-Implicit Arguments af_level2 [[A] [level] [age1]].
+Arguments af_unage {A level age1}.
+Arguments af_level1 {A level age1}.
+Arguments af_level2 {A level age1}.
 
 Class ageable (A:Type) := mkAgeable
 { level : A -> nat
@@ -77,7 +77,7 @@ Coercion app_pred : pred >-> Funclass.
 Global Opaque pred.
 
 Definition derives {A} `{ageable A} (P Q:pred A) := forall a:A, P a -> Q a.
-Implicit Arguments derives.
+Arguments derives : default implicits.
 
 Program Definition andp {A} `{ageable A} (P Q:pred A) : pred A :=
    fun a:A => P a /\ Q a.
@@ -170,7 +170,7 @@ Class Functor `(C:Category) `(D:Category) (im : C -> D) := {
     fmap g ∘ fmap f ≈ fmap (g ∘ f)
 }.
 Coercion functor_im : Functor >-> Funclass.
-Implicit Arguments fmap [Object Hom C Object0 Hom0 D im a b].
+Arguments fmap [Object Hom C Object0 Hom0 D im] _ [a b].
 
 Add Parametric Morphism `(C:Category) `(D:Category)
   (Im:C->D) (F:Functor C D Im) (a b:C) : (@fmap _ _ C _ _ D Im F a b)
diff --git a/test-suite/bugs/closed/3068.v b/test-suite/bugs/closed/3068.v
index 79671ce93..9811733dc 100644
--- a/test-suite/bugs/closed/3068.v
+++ b/test-suite/bugs/closed/3068.v
@@ -33,7 +33,7 @@ Section Counted_list.
 
 End Counted_list.
 
-Implicit Arguments counted_def_nth [A n].
+Arguments counted_def_nth [A n].
 
 Section Finite_nat_set.
 
diff --git a/test-suite/bugs/closed/3513.v b/test-suite/bugs/closed/3513.v
index 1f0f3b0da..a1d0b9107 100644
--- a/test-suite/bugs/closed/3513.v
+++ b/test-suite/bugs/closed/3513.v
@@ -21,7 +21,7 @@ Section ILogic_Fun.
   Local Instance ILFun_Ops : ILogicOps (@ILFunFrm T _ Frm _) := admit.
   Definition ILFun_ILogic : ILogic (@ILFunFrm T _ Frm _) := admit.
 End ILogic_Fun.
-Implicit Arguments ILFunFrm [[ILOps] [e]].
+Arguments ILFunFrm _ {e} _ {ILOps}.
 Instance ILogicOps_Prop : ILogicOps Prop | 2 := {| lentails P Q := (P : Prop) -> Q;
                                                    ltrue        := True;
                                                    land     P Q := P /\ Q;
diff --git a/test-suite/bugs/closed/3647.v b/test-suite/bugs/closed/3647.v
index f5a22bd50..e91c004c7 100644
--- a/test-suite/bugs/closed/3647.v
+++ b/test-suite/bugs/closed/3647.v
@@ -26,7 +26,7 @@ Record morphism T T' `{e : type T} `{e' : type T'} :=
   mkMorph {
       morph :> T -> T';
       morph_resp : setoid_resp morph}.
-Implicit Arguments mkMorph [T T' e e0 e' e1].
+Arguments mkMorph [T T' e0 e e1 e'].
 Infix "-s>" := morphism (at level 45, right associativity).
 Section Morphisms.
   Context {S T U V} `{eS : type S} `{eT : type T} `{eU : type U} `{eV : type V}.
@@ -334,8 +334,8 @@ Section ILogic_Fun.
 
 End ILogic_Fun.
 
-Implicit Arguments ILFunFrm [[ILOps] [e]].
-Implicit Arguments mkILFunFrm [T Frm ILOps].
+Arguments ILFunFrm _ {e} _ {ILOps}.
+Arguments mkILFunFrm [T] _ [Frm ILOps].
 
 Program Definition ILFun_eq {T R} {ILOps: ILogicOps R} {ILogic: ILogic R} (P : T -> R) :
   @ILFunFrm T _ R ILOps :=
diff --git a/test-suite/bugs/closed/3732.v b/test-suite/bugs/closed/3732.v
index 09f1149c2..13d62b8ff 100644
--- a/test-suite/bugs/closed/3732.v
+++ b/test-suite/bugs/closed/3732.v
@@ -16,7 +16,7 @@ Section machine.
   | Inj : forall G, Prop -> propX G
   | ExistsX : forall G A, propX (A :: G) -> propX G.
 
-  Implicit Arguments Inj [G].
+  Arguments Inj [G].
 
   Definition PropX := propX nil.
   Fixpoint last (G : list Type) : Type.
diff --git a/test-suite/bugs/closed/4095.v b/test-suite/bugs/closed/4095.v
index 8d7dfbd49..bc9380f90 100644
--- a/test-suite/bugs/closed/4095.v
+++ b/test-suite/bugs/closed/4095.v
@@ -23,7 +23,7 @@ Section ILogic_Fun.
   Local Instance ILFun_Ops : ILogicOps (@ILFunFrm T _ Frm _) := admit.
   Definition ILFun_ILogic : ILogic (@ILFunFrm T _ Frm _) := admit.
 End ILogic_Fun.
-Implicit Arguments ILFunFrm [[ILOps] [e]].
+Arguments ILFunFrm _ {e} _ {ILOps}.
 Instance ILogicOps_Prop : ILogicOps Prop | 2 := {| lentails P Q := (P : Prop) -> Q;
                                                    ltrue        := True;
                                                    land     P Q := P /\ Q;
diff --git a/test-suite/bugs/closed/4865.v b/test-suite/bugs/closed/4865.v
index c5bf3289b..da4e53aab 100644
--- a/test-suite/bugs/closed/4865.v
+++ b/test-suite/bugs/closed/4865.v
@@ -48,5 +48,5 @@ Fail Check g 0 0 1. (* 2nd 0 in bool *)
 Fixpoint arr n := match n with 0%nat => nat | S n => nat -> arr n end.
 Fixpoint lam n : arr n := match n with 0%nat => 0%nat | S n => fun x => lam n  end.
 Notation "0" := true.
-Arguments Scope lam [nat_scope nat_scope].
+Arguments lam _%nat_scope _%nat_scope : extra scopes.
 Check (lam 1 0).
diff --git a/test-suite/bugs/opened/2456.v b/test-suite/bugs/opened/2456.v
index 6cca5c9fb..5294adefd 100644
--- a/test-suite/bugs/opened/2456.v
+++ b/test-suite/bugs/opened/2456.v
@@ -6,7 +6,7 @@ Parameter Patch : nat -> nat -> Set.
 Inductive Catch (from to : nat) : Type
     := MkCatch : forall (p : Patch from to),
                  Catch from to.
-Implicit Arguments MkCatch [from to].
+Arguments MkCatch [from to].
 
 Inductive CatchCommute5
         : forall {from mid1 mid2 to : nat},
diff --git a/test-suite/bugs/opened/3295.v b/test-suite/bugs/opened/3295.v
index 2a156e333..c09649de7 100644
--- a/test-suite/bugs/opened/3295.v
+++ b/test-suite/bugs/opened/3295.v
@@ -5,7 +5,7 @@ Class lops := lmk_ops {
   weq: relation car
 }.
 
-Implicit Arguments car [].
+Arguments car : clear implicits.
 
 Coercion car: lops >-> Sortclass.
 
@@ -23,7 +23,7 @@ Class ops := mk_ops {
   dot: forall n m p, mor n m -> mor m p -> mor n p
 }.
 Coercion mor: ops >-> Funclass.
-Implicit Arguments ob [].
+Arguments ob : clear implicits.
 
 Instance dot_weq `{ops} n m p: Proper (weq ==> weq ==> weq) (dot n m p).
 Proof.
diff --git a/test-suite/complexity/injection.v b/test-suite/complexity/injection.v
index 08f489d75..a76fa19d3 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.
-Implicit Arguments ADMIT [p].
+Arguments ADMIT [p].
 
 Module Share.
 Parameter jb : joinable bool.
diff --git a/test-suite/failure/check.v b/test-suite/failure/check.v
index a148ebe8e..0ef4b417a 100644
--- a/test-suite/failure/check.v
+++ b/test-suite/failure/check.v
@@ -1,3 +1,3 @@
-Implicit Arguments eq [A].
+Arguments eq [A].
 
 Fail Check (bool = true).
diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v
index 8ba8525c6..be3310491 100644
--- a/test-suite/modules/PO.v
+++ b/test-suite/modules/PO.v
@@ -1,8 +1,8 @@
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Implicit Arguments fst.
-Implicit Arguments snd.
+Arguments fst : default implicits.
+Arguments snd : default implicits.
 
 Module Type PO.
   Parameter T : Set.
diff --git a/test-suite/modules/Przyklad.v b/test-suite/modules/Przyklad.v
index 7214287a6..ece1b47b4 100644
--- a/test-suite/modules/Przyklad.v
+++ b/test-suite/modules/Przyklad.v
@@ -1,7 +1,7 @@
 Definition ifte (T : Set) (A B : Prop) (s : {A} + {B})
   (th el : T) := if s then th else el.
 
-Implicit Arguments ifte.
+Arguments ifte : default implicits.
 
 Lemma Reflexivity_provable :
  forall (A : Set) (a : A) (s : {a = a} + {a <> a}),
diff --git a/test-suite/prerequisite/make_local.v b/test-suite/prerequisite/make_local.v
index 8700a6c4e..6d9117c05 100644
--- a/test-suite/prerequisite/make_local.v
+++ b/test-suite/prerequisite/make_local.v
@@ -2,8 +2,7 @@
 
 Definition f (A:Type) (a:A) := a.
 
-Local Arguments Scope f [type_scope type_scope].
-Local Implicit Arguments f [A].
+Local Arguments f [A]%type_scope _%type_scope.
 
 (* Used in ImportedCoercion.v to test the locality flag *)
 
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.