theories/, plugins/ and test-suite/ ported to the Arguments vernacular

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14718 85f007b7-540e-0410-9357-904b9bb8a0f7

38 files changed, 135 insertions, 137 deletions

diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v
index 1dd5ce16c..146546dc1 100644
--- a/theories/Arith/Factorial.v
+++ b/theories/Arith/Factorial.v
@@ -19,7 +19,7 @@ Fixpoint fact (n:nat) : nat :=
     | S n => S n * fact n
   end.
 
-Arguments Scope fact [nat_scope].
+Arguments fact n%nat.
 
 Lemma lt_O_fact : forall n:nat, 0 < fact n.
 Proof.
diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v
index 73a092143..24b6a7760 100644
--- a/theories/Bool/Sumbool.v
+++ b/theories/Bool/Sumbool.v
@@ -66,4 +66,4 @@ Definition bool_of_sumbool :
   intros A B H.
   elim H; intro; [exists true | exists false]; assumption.
 Defined.
-Implicit Arguments bool_of_sumbool.
+Arguments bool_of_sumbool : default implicits.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 55199cdea..8e491b1b8 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -55,8 +55,8 @@ Definition respectful {A B : Type}
 
 Delimit Scope signature_scope with signature.
 
-Arguments Scope Proper [type_scope signature_scope].
-Arguments Scope respectful [type_scope type_scope signature_scope signature_scope].
+Arguments Proper {A}%type R%signature m.
+Arguments respectful {A B}%type (R R')%signature _ _.
 
 Module ProperNotations.
 
@@ -121,7 +121,7 @@ Definition forall_relation {A : Type} {B : A -> Type}
  (sig : forall a, relation (B a)) : relation (forall x, B x) :=
  fun f g => forall a, sig a (f a) (g a).
 
-Arguments Scope forall_relation [type_scope type_scope signature_scope].
+Arguments forall_relation {A B}%type sig%signature _ _.
 
 (** Non-dependent pointwise lifting *)
 
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 3a34e3a11..cf05d9d4c 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -351,7 +351,7 @@ Definition relation_equivalence {A : Type} : relation (relation A) :=
 Class subrelation {A:Type} (R R' : relation A) : Prop :=
   is_subrelation : @predicate_implication (A::A::Tnil) R R'.
 
-Implicit Arguments subrelation [[A]].
+Arguments subrelation {A} R R'.
 
 Definition relation_conjunction {A} (R : relation A) (R' : relation A) : relation A :=
   @predicate_intersection (A::A::Tnil) R R'.
diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v
index 0fa5bfaa6..2b010206c 100644
--- a/theories/Classes/RelationPairs.v
+++ b/theories/Classes/RelationPairs.v
@@ -15,27 +15,25 @@ Require Import Relations Morphisms.
     fix the simpl tactic, since "simpl fst" would be refused for
     the moment.
 
-Implicit Arguments fst [[A] [B]].
-Implicit Arguments snd [[A] [B]].
-Implicit Arguments pair [[A] [B]].
+Arguments fst {A B}.
+Arguments snd {A B}.
+Arguments pair {A B}.
 
 /NB *)
 
 Local Notation Fst := (@fst _ _).
 Local Notation Snd := (@snd _ _).
 
-Arguments Scope relation_conjunction
- [type_scope signature_scope signature_scope].
-Arguments Scope relation_equivalence
- [type_scope signature_scope signature_scope].
-Arguments Scope subrelation [type_scope signature_scope signature_scope].
-Arguments Scope Reflexive [type_scope signature_scope].
-Arguments Scope Irreflexive [type_scope signature_scope].
-Arguments Scope Symmetric [type_scope signature_scope].
-Arguments Scope Transitive [type_scope signature_scope].
-Arguments Scope PER [type_scope signature_scope].
-Arguments Scope Equivalence [type_scope signature_scope].
-Arguments Scope StrictOrder [type_scope signature_scope].
+Arguments relation_conjunction A%type (R R')%signature _ _.
+Arguments relation_equivalence A%type (_ _)%signature.
+Arguments subrelation A%type (R R')%signature.
+Arguments Reflexive A%type R%signature.
+Arguments Irreflexive A%type R%signature.
+Arguments Symmetric A%type R%signature.
+Arguments Transitive A%type R%signature.
+Arguments PER A%type R%signature.
+Arguments Equivalence A%type R%signature.
+Arguments StrictOrder A%type R%signature.
 
 Generalizable Variables A B RA RB Ri Ro f.
 
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 7665ac05b..0c1448c9b 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -652,7 +652,7 @@ Add Relation key E.eq
  transitivity proved by E.eq_trans
  as KeySetoid.
 
-Implicit Arguments Equal [[elt]].
+Arguments Equal {elt} m m'.
 
 Add Parametric Relation (elt : Type) : (t elt) Equal
  reflexivity proved by (@Equal_refl elt)
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index 206714949..2e2eb166d 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -84,7 +84,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   Section A.
   Variable A:Type.
 
-  Implicit Arguments Leaf [A].
+  Arguments Leaf [A].
 
   Definition empty : t A := Leaf.
 
@@ -814,7 +814,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   Variable A B C : Type.
   Variable f : option A -> option B -> option C.
 
-  Implicit Arguments Leaf [A].
+  Arguments Leaf [A].
 
   Fixpoint xmap2_l (m : t A) : t C :=
       match m with
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index bab764bcb..41f6b70b2 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -137,7 +137,7 @@ Inductive nat : Set :=
 
 Delimit Scope nat_scope with nat.
 Bind Scope nat_scope with nat.
-Arguments Scope S [nat_scope].
+Arguments S _%nat.
 
 
 (********************************************************************)
@@ -149,7 +149,7 @@ Inductive option (A:Type) : Type :=
   | Some : A -> option A
   | None : option A.
 
-Implicit Arguments None [A].
+Arguments None [A].
 
 Definition option_map (A B:Type) (f:A->B) o :=
   match o with
@@ -165,8 +165,8 @@ Inductive sum (A B:Type) : Type :=
 
 Notation "x + y" := (sum x y) : type_scope.
 
-Implicit Arguments inl [[A] [B]] [A].
-Implicit Arguments inr [[A] [B]] [B].
+Arguments inl {A B} _ , [A] B _.
+Arguments inr {A B} _ , A [B] _.
 
 (** [prod A B], written [A * B], is the product of [A] and [B];
     the pair [pair A B a b] of [a] and [b] is abbreviated [(a,b)] *)
@@ -179,7 +179,7 @@ Add Printing Let prod.
 Notation "x * y" := (prod x y) : type_scope.
 Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
 
-Implicit Arguments pair [[A] [B]].
+Arguments pair {A B} _ _.
 
 Section projections.
   Variables A B : Type.
@@ -221,7 +221,7 @@ Inductive list (A : Type) : Type :=
  | nil : list A
  | cons : A -> list A -> list A.
 
-Implicit Arguments nil [A].
+Arguments nil [A].
 Infix "::" := cons (at level 60, right associativity) : list_scope.
 Delimit Scope list_scope with list.
 Bind Scope list_scope with list.
@@ -330,9 +330,9 @@ Inductive identity (A:Type) (a:A) : A -> Type :=
   identity_refl : identity a a.
 Hint Resolve identity_refl: core.
 
-Implicit Arguments identity_ind [A].
-Implicit Arguments identity_rec [A].
-Implicit Arguments identity_rect [A].
+Arguments identity_ind [A] a P f y i.
+Arguments identity_rec [A] a P f y i.
+Arguments identity_rect [A] a P f y i.
 
 (** Identity type *)
 
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index b9e22f15e..d1eabcabf 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -62,8 +62,8 @@ Inductive or (A B:Prop) : Prop :=
 
 where "A \/ B" := (or A B) : type_scope.
 
-Implicit Arguments or_introl [A B] [A].
-Implicit Arguments or_intror [A B] [B].
+Arguments or_introl [A B] _, [A] B _.
+Arguments or_intror [A B] _, A [B] _.
 
 (** [iff A B], written [A <-> B], expresses the equivalence of [A] and [B] *)
 
@@ -270,12 +270,12 @@ Notation "x = y" := (x = y :>_) : type_scope.
 Notation "x <> y  :> T" := (~ x = y :>T) : type_scope.
 Notation "x <> y" := (x <> y :>_) : type_scope.
 
-Implicit Arguments eq [[A]].
-Implicit Arguments eq_refl [[A] [x]] [A].
+Arguments eq {A} x _.
+Arguments eq_refl {A x} , [A] x.
 
-Implicit Arguments eq_ind [A].
-Implicit Arguments eq_rec [A].
-Implicit Arguments eq_rect [A].
+Arguments eq_ind [A] x P _ y _.
+Arguments eq_rec [A] x P _ y _.
+Arguments eq_rect [A] x P _ y _.
 
 Hint Resolve I conj or_introl or_intror eq_refl: core.
 Hint Resolve ex_intro ex_intro2: core.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 12ac08ff0..637994b2b 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -38,10 +38,10 @@ Inductive sigT2 (A:Type) (P Q:A -> Type) : Type :=
 
 (* Notations *)
 
-Arguments Scope sig [type_scope type_scope].
-Arguments Scope sig2 [type_scope type_scope type_scope].
-Arguments Scope sigT [type_scope type_scope].
-Arguments Scope sigT2 [type_scope type_scope type_scope].
+Arguments sig (A P)%type.
+Arguments sig2 (A P Q)%type.
+Arguments sigT (A P)%type.
+Arguments sigT2 (A P Q)%type.
 
 Notation "{ x  |  P }" := (sig (fun x => P)) : type_scope.
 Notation "{ x  |  P  & Q }" := (sig2 (fun x => P) (fun x => Q)) : type_scope.
@@ -126,8 +126,8 @@ Inductive sumbool (A B:Prop) : Set :=
 
 Add Printing If sumbool.
 
-Implicit Arguments left [[A] [B]] [A].
-Implicit Arguments right [[A] [B]] [B].
+Arguments left {A B} _, [A] B _.
+Arguments right {A B} _ , A [B] _.
 
 (** [sumor] is an option type equipped with the justification of why
     it may not be a regular value *)
@@ -139,8 +139,8 @@ Inductive sumor (A:Type) (B:Prop) : Type :=
 
 Add Printing If sumor.
 
-Implicit Arguments inleft [[A] [B]] [A].
-Implicit Arguments inright [[A] [B]] [B].
+Arguments inleft {A B} _ , [A] B _.
+Arguments inright {A B} _ , A [B] _.
 
 (** Various forms of the axiom of choice for specifications *)
 
@@ -208,11 +208,11 @@ Definition Exc := option.
 Definition value := Some.
 Definition error := @None.
 
-Implicit Arguments error [A].
+Arguments error [A].
 
 Definition except := False_rec. (* for compatibility with previous versions *)
 
-Implicit Arguments except [P].
+Arguments except [P] _.
 
 Theorem absurd_set : forall (A:Prop) (C:Set), A -> ~ A -> C.
 Proof.
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index ef319529d..97915055d 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -748,7 +748,7 @@ rewrite filter_In in H; destruct H.
 eapply SortA_InfA_InA; eauto.
 Qed.
 
-Implicit Arguments eq [ [A] ].
+Arguments eq {A} x _.
 
 Lemma filter_InA : forall f, Proper (eqA==>eq) f ->
  forall l x, InA x (List.filter f l) <-> InA x l /\ f x = true.
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index a341a7a5a..d84cd8240 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.v
@@ -107,8 +107,8 @@ Section Dependent_Equality.
 
 End Dependent_Equality.
 
-Implicit Arguments eq_dep [U P].
-Implicit Arguments eq_dep1 [U P].
+Arguments eq_dep  [U P] p x q _.
+Arguments eq_dep1 [U P] p x q y.
 
 (** Dependent equality is equivalent to equality on dependent pairs *)
 
@@ -412,5 +412,5 @@ Notation inj_pairT2 := inj_pair2.
 
 End EqdepTheory.
 
-Implicit Arguments eq_dep [].
-Implicit Arguments eq_dep1 [].
+Arguments eq_dep  U P p x q _ : clear implicits.
+Arguments eq_dep1 U P p x q y : clear implicits.
diff --git a/theories/Logic/ExtensionalityFacts.v b/theories/Logic/ExtensionalityFacts.v
index 421bbebcf..f5e71ef49 100644
--- a/theories/Logic/ExtensionalityFacts.v
+++ b/theories/Logic/ExtensionalityFacts.v
@@ -42,8 +42,8 @@ Record Delta A := { pi1:A; pi2:A; eq:pi1=pi2 }.
 
 Definition delta {A} (a:A) := {|pi1 := a; pi2 := a; eq := eq_refl a |}.
 
-Implicit Arguments pi1 [[A]].
-Implicit Arguments pi2 [[A]].
+Arguments pi1 {A} _.
+Arguments pi2 {A} _.
 
 Lemma diagonal_projs_same_behavior : forall A (x:Delta A), pi1 x = pi2 x.
 Proof.
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index 583d348a2..753009e68 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -24,7 +24,7 @@ Inductive JMeq (A:Type) (x:A) : forall B:Type, B -> Prop :=
 
 Set Elimination Schemes.
 
-Implicit Arguments JMeq_refl [[A] [x]] [A].
+Arguments JMeq_refl {A x} , [A] x.
 
 Hint Resolve JMeq_refl.
 
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index 1e2ddb7a6..bdada4868 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -375,7 +375,7 @@ Fixpoint fold (A : Type) (f : elt -> A -> A)(s : t) : A -> A :=
   | Leaf => a
   | Node l x r _ => fold f r (f x (fold f l a))
  end.
-Implicit Arguments fold [A].
+Arguments fold [A] f s _.
 
 
 (** ** Subset *)
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index 20504bcf8..f2b908af0 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -437,7 +437,7 @@ Module WRaw2SetsOn (E:DecidableType)(M:WRawSets E) <: WSetsOn E.
 
  Record t_ := Mkt {this :> M.t; is_ok : M.Ok this}.
  Definition t := t_.
- Implicit Arguments Mkt [ [is_ok] ].
+ Arguments Mkt this {is_ok}.
  Hint Resolve is_ok : typeclass_instances.
 
  Definition In (x : elt)(s : t) := M.In x s.(this).
diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v
index 69754f144..dfb2c5025 100644
--- a/theories/Numbers/BinNums.v
+++ b/theories/Numbers/BinNums.v
@@ -27,8 +27,8 @@ Inductive positive : Set :=
 
 Delimit Scope positive_scope with positive.
 Bind Scope positive_scope with positive.
-Arguments Scope xO [positive_scope].
-Arguments Scope xI [positive_scope].
+Arguments xO _%positive.
+Arguments xI _%positive.
 
 (** [N] is a datatype representing natural numbers in a binary way,
     by extending the [positive] datatype with a zero.
@@ -41,7 +41,7 @@ Inductive N : Set :=
 
 Delimit Scope N_scope with N.
 Bind Scope N_scope with N.
-Arguments Scope Npos [positive_scope].
+Arguments Npos _%positive.
 
 (** [Z] is a datatype representing the integers in a binary way.
     An integer is either zero or a strictly positive number
@@ -57,5 +57,5 @@ Inductive Z : Set :=
 
 Delimit Scope Z_scope with Z.
 Bind Scope Z_scope with Z.
-Arguments Scope Zpos [positive_scope].
-Arguments Scope Zneg [positive_scope].
+Arguments Zpos _%positive.
+Arguments Zneg _%positive.
diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index 3aa075384..59656eedb 100644
--- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
+++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
@@ -204,7 +204,7 @@ Module ZnZ.
 
  End Specs.
 
- Implicit Arguments Specs [[t]].
+ Arguments Specs {t} ops.
 
  (** Generic construction of double words *)
 
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
index 073afec37..a274b8395 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
@@ -53,7 +53,7 @@ Section Zn2Z.
 
 End Zn2Z.
 
-Implicit Arguments W0 [znz].
+Arguments W0 [znz].
 
 (** From a cyclic representation [w], we iterate the [zn2z] construct
     [n] times, gaining the type of binary trees of depth at most [n],
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 71d275601..443777f52 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -44,8 +44,8 @@ Local Open Scope bigZ_scope.
 
 Notation bigZ := BigZ.t.
 Bind Scope bigZ_scope with bigZ BigZ.t BigZ.t_.
-Arguments Scope BigZ.Pos [bigN_scope].
-Arguments Scope BigZ.Neg [bigN_scope].
+Arguments BigZ.Pos _%bigN.
+Arguments BigZ.Neg _%bigN.
 Local Notation "0" := BigZ.zero : bigZ_scope.
 Local Notation "1" := BigZ.one : bigZ_scope.
 Local Notation "2" := BigZ.two : bigZ_scope.
diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v
index 8df715af9..ad7a9f3ae 100644
--- a/theories/Numbers/Natural/Abstract/NDefOps.v
+++ b/theories/Numbers/Natural/Abstract/NDefOps.v
@@ -23,7 +23,7 @@ Include NStrongRecProp N.
 Definition if_zero (A : Type) (a b : A) (n : N.t) : A :=
   recursion a (fun _ _ => b) n.
 
-Implicit Arguments if_zero [A].
+Arguments if_zero [A] a b n.
 
 Instance if_zero_wd (A : Type) :
  Proper (Logic.eq ==> Logic.eq ==> N.eq ==> Logic.eq) (@if_zero A).
diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v
index 039eefdf5..607746d59 100644
--- a/theories/Numbers/Natural/Abstract/NStrongRec.v
+++ b/theories/Numbers/Natural/Abstract/NStrongRec.v
@@ -190,7 +190,7 @@ Qed.
 End FixPoint.
 End StrongRecursion.
 
-Implicit Arguments strong_rec [A].
+Arguments strong_rec [A] a f n.
 
 End NStrongRecProp.
 
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index b06e42ca2..7f205b388 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -52,7 +52,7 @@ Local Open Scope bigN_scope.
 
 Notation bigN := BigN.t.
 Bind Scope bigN_scope with bigN BigN.t BigN.t'.
-Arguments Scope BigN.N0 [int31_scope].
+Arguments BigN.N0 _%int31.
 Local Notation "0" := BigN.zero : bigN_scope. (* temporary notation *)
 Local Notation "1" := BigN.one : bigN_scope. (* temporary notation *)
 Local Notation "2" := BigN.two : bigN_scope. (* temporary notation *)
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index 668a11123..3ea3d5fd5 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -705,7 +705,7 @@ pr
 
  End SameLevel.
 
- Implicit Arguments same_level [res].
+ Arguments same_level [res] f x y.
 
  Theorem spec_same_level_dep :
   forall res
diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v
index aed96a831..4717d0b23 100644
--- a/theories/Numbers/Natural/BigN/Nbasic.v
+++ b/theories/Numbers/Natural/BigN/Nbasic.v
@@ -16,12 +16,12 @@ Require Import DoubleBase.
 Require Import CyclicAxioms.
 Require Import DoubleCyclic.
 
-Implicit Arguments mk_zn2z_ops [t].
-Implicit Arguments mk_zn2z_ops_karatsuba [t].
-Implicit Arguments mk_zn2z_specs [t ops].
-Implicit Arguments mk_zn2z_specs_karatsuba [t ops].
-Implicit Arguments ZnZ.digits [t].
-Implicit Arguments ZnZ.zdigits [t].
+Arguments mk_zn2z_ops [t] ops.
+Arguments mk_zn2z_ops_karatsuba [t] ops.
+Arguments mk_zn2z_specs [t ops] specs.
+Arguments mk_zn2z_specs_karatsuba [t ops] specs.
+Arguments ZnZ.digits [t] Ops.
+Arguments ZnZ.zdigits [t] Ops.
 
 Lemma Pshiftl_nat_Zpower : forall n p,
   Zpos (Pos.shiftl_nat p n) = Zpos p * 2 ^ Z.of_nat n.
@@ -230,8 +230,8 @@ Fixpoint extend_tr (n : nat) {struct n}: (word w (S (n + m))) :=
 
 End ExtendMax.
 
-Implicit Arguments extend_tr[w m].
-Implicit Arguments castm[w m n].
+Arguments extend_tr [w m] v n.
+Arguments castm     [w m n] H x.
 
 
 
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index a0ad7643d..2c7884ac4 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -445,7 +445,7 @@ Qed.
 
 Definition recursion (A : Type) (a : A) (f : NN.t -> A -> A) (n : NN.t) :=
   Nrect (fun _ => A) a (fun n a => f (NN.of_N n) a) (NN.to_N n).
-Implicit Arguments recursion [A].
+Arguments recursion [A] a f n.
 
 Instance recursion_wd (A : Type) (Aeq : relation A) :
  Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) (@recursion A).
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index 5293a66cb..7cef5c5ad 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -17,7 +17,7 @@
 
 (** The polymorphic identity function is defined in [Datatypes]. *)
 
-Implicit Arguments id [[A]].
+Arguments id {A} x.
 
 (** Function composition. *)
 
@@ -53,5 +53,5 @@ Definition apply {A B} (f : A -> B) (x : A) := f x.
 
 (** Curryfication of [prod] is defined in [Logic.Datatypes]. *)
 
-Implicit Arguments prod_curry [[A] [B] [C]].
-Implicit Arguments prod_uncurry [[A] [B] [C]].
+Arguments prod_curry   {A B C} f p.
+Arguments prod_uncurry {A B C} f x y.
diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v
index a66e1284b..61d389ed5 100644
--- a/theories/Program/Syntax.v
+++ b/theories/Program/Syntax.v
@@ -18,15 +18,15 @@ Notation " () " := tt.
 
 (** Set maximally inserted implicit arguments for standard definitions. *)
 
-Implicit Arguments Some [[A]].
-Implicit Arguments None [[A]].
+Arguments Some {A} _.
+Arguments None {A}.
 
-Implicit Arguments pair [[A] [B]].
-Implicit Arguments fst [[A] [B]].
-Implicit Arguments snd [[A] [B]].
+Arguments pair {A B} _ _.
+Arguments fst {A B} _.
+Arguments snd {A B} _.
 
-Implicit Arguments nil [[A]].
-Implicit Arguments cons [[A]].
+Arguments nil {A}.
+Arguments cons {A} _ _.
 
 Require List.
 Export List.ListNotations.
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index a32ccbc4b..94ea4906c 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -18,7 +18,7 @@ Record Q : Set := Qmake {Qnum : Z; Qden : positive}.
 
 Delimit Scope Q_scope with Q.
 Bind Scope Q_scope with Q.
-Arguments Scope Qmake [Z_scope positive_scope].
+Arguments Qmake _%Z _%positive.
 Open Scope Q_scope.
 Ltac simpl_mult := repeat rewrite Zpos_mult_morphism.
 
@@ -27,7 +27,7 @@ Ltac simpl_mult := repeat rewrite Zpos_mult_morphism.
 Notation "a # b" := (Qmake a b) (at level 55, no associativity) : Q_scope.
 
 Definition inject_Z (x : Z) := Qmake x 1.
-Arguments Scope inject_Z [Z_scope].
+Arguments inject_Z x%Z.
 
 Notation QDen p := (Zpos (Qden p)).
 Notation " 0 " := (0#1) : Q_scope.
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v
index 218289a4f..fea2ba398 100644
--- a/theories/QArith/Qcanon.v
+++ b/theories/QArith/Qcanon.v
@@ -18,7 +18,7 @@ Record Qc : Set := Qcmake { this :> Q ; canon : Qred this = this }.
 
 Delimit Scope Qc_scope with Qc.
 Bind Scope Qc_scope with Qc.
-Arguments Scope Qcmake [Q_scope].
+Arguments Qcmake this%Q _.
 Open Scope Qc_scope.
 
 Lemma Qred_identity :
@@ -69,7 +69,7 @@ Proof.
 Qed.
 
 Definition Q2Qc (q:Q) : Qc := Qcmake (Qred q) (Qred_involutive q).
-Arguments Scope Q2Qc [Q_scope].
+Arguments Q2Qc q%Q.
 Notation " !! " := Q2Qc : Qc_scope.
 
 Lemma Qc_is_canon : forall q q' : Qc, q == q' -> q = q'.
diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v
index 18cf53e71..3075bee8f 100644
--- a/theories/Reals/Ranalysis1.v
+++ b/theories/Reals/Ranalysis1.v
@@ -28,15 +28,15 @@ Definition inv_fct f (x:R) : R := / f x.
 
 Delimit Scope Rfun_scope with F.
 
-Arguments Scope plus_fct [Rfun_scope Rfun_scope R_scope].
-Arguments Scope mult_fct [Rfun_scope Rfun_scope R_scope].
-Arguments Scope minus_fct [Rfun_scope Rfun_scope R_scope].
-Arguments Scope div_fct [Rfun_scope Rfun_scope R_scope].
-Arguments Scope inv_fct [Rfun_scope R_scope].
-Arguments Scope opp_fct [Rfun_scope R_scope].
-Arguments Scope mult_real_fct [R_scope Rfun_scope R_scope].
-Arguments Scope div_real_fct [R_scope Rfun_scope R_scope].
-Arguments Scope comp [Rfun_scope Rfun_scope R_scope].
+Arguments plus_fct (f1 f2)%F x%R.
+Arguments mult_fct (f1 f2)%F x%R.
+Arguments minus_fct (f1 f2)%F x%R.
+Arguments div_fct (f1 f2)%F x%R.
+Arguments inv_fct f%F x%R.
+Arguments opp_fct f%F x%R.
+Arguments mult_real_fct a%R f%F x%R.
+Arguments div_real_fct a%R f%F x%R.
+Arguments comp (f1 f2)%F x%R.
 
 Infix "+" := plus_fct : Rfun_scope.
 Notation "- x" := (opp_fct x) : Rfun_scope.
@@ -74,8 +74,8 @@ Definition constant_D_eq f (D:R -> Prop) (c:R) : Prop :=
 Definition continuity_pt f (x0:R) : Prop := continue_in f no_cond x0.
 Definition continuity f : Prop := forall x:R, continuity_pt f x.
 
-Arguments Scope continuity_pt [Rfun_scope R_scope].
-Arguments Scope continuity [Rfun_scope].
+Arguments continuity_pt f%F x0%R.
+Arguments continuity f%F.
 
 (**********)
 Lemma continuity_pt_plus :
@@ -274,12 +274,12 @@ Definition derivable f := forall x:R, derivable_pt f x.
 Definition derive_pt f (x:R) (pr:derivable_pt f x) := proj1_sig pr.
 Definition derive f (pr:derivable f) (x:R) := derive_pt f x (pr x).
 
-Arguments Scope derivable_pt_lim [Rfun_scope R_scope].
-Arguments Scope derivable_pt_abs [Rfun_scope R_scope R_scope].
-Arguments Scope derivable_pt [Rfun_scope R_scope].
-Arguments Scope derivable [Rfun_scope].
-Arguments Scope derive_pt [Rfun_scope R_scope _].
-Arguments Scope derive [Rfun_scope _].
+Arguments derivable_pt_lim f%F x%R l.
+Arguments derivable_pt_abs f%F (x l)%R.
+Arguments derivable_pt f%F x%R.
+Arguments derivable f%F.
+Arguments derive_pt f%F x%R pr.
+Arguments derive f%F pr x.
 
 Definition antiderivative f (g:R -> R) (a b:R) : Prop :=
   (forall x:R,
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index e858d2148..8f01d7d03 100644
--- a/theories/Reals/Raxioms.v
+++ b/theories/Reals/Raxioms.v
@@ -111,7 +111,7 @@ Fixpoint INR (n:nat) : R :=
   | S O => 1
   | S n => INR n + 1
   end.
-Arguments Scope INR [nat_scope].
+Arguments INR n%nat.
 
 
 (**********************************************************)
@@ -125,7 +125,7 @@ Definition IZR (z:Z) : R :=
   | Zpos n => INR (nat_of_P n)
   | Zneg n => - INR (nat_of_P n)
   end.
-Arguments Scope IZR [Z_scope].
+Arguments IZR z%Z.
 
 (**********************************************************)
 (** *    [R] Archimedean                                  *)
diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v
index 21beac36f..f7f5512e7 100644
--- a/theories/Relations/Operators_Properties.v
+++ b/theories/Relations/Operators_Properties.v
@@ -17,17 +17,17 @@ Require Import Relation_Operators.
 
 Section Properties.
 
-  Implicit Arguments clos_refl_trans [A].
-  Implicit Arguments clos_refl_trans_1n [A].
-  Implicit Arguments clos_refl_trans_n1 [A].
-  Implicit Arguments clos_refl_sym_trans [A].
-  Implicit Arguments clos_refl_sym_trans_1n [A].
-  Implicit Arguments clos_refl_sym_trans_n1 [A].
-  Implicit Arguments clos_trans [A].
-  Implicit Arguments clos_trans_1n [A].
-  Implicit Arguments clos_trans_n1 [A].
-  Implicit Arguments inclusion [A].
-  Implicit Arguments preorder [A].
+  Arguments clos_refl_trans [A] R x _.
+  Arguments clos_refl_trans_1n [A] R x _.
+  Arguments clos_refl_trans_n1 [A] R x _.
+  Arguments clos_refl_sym_trans [A] R _ _.
+  Arguments clos_refl_sym_trans_1n [A] R x _.
+  Arguments clos_refl_sym_trans_n1 [A] R x _.
+  Arguments clos_trans [A] R x _.
+  Arguments clos_trans_1n [A] R x _.
+  Arguments clos_trans_n1 [A] R x _.
+  Arguments inclusion [A] R1 R2.
+  Arguments preorder [A] R.
 
   Variable A : Type.
   Variable R : relation A.
diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v
index cdca469ac..0e230b77b 100644
--- a/theories/Sorting/Sorted.v
+++ b/theories/Sorting/Sorted.v
@@ -25,7 +25,7 @@ Require Import List Relations Relations_1.
 Set Implicit Arguments.
 Local Notation "[ ]" := nil (at level 0).
 Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) (at level 0).
-Implicit Arguments Transitive [U].
+Arguments Transitive [U] R.
 
 Section defs.
 
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index 5d8773957..f84cdf32c 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -20,9 +20,9 @@ Inductive Compare (X : Type) (lt eq : X -> X -> Prop) (x y : X) : Type :=
   | EQ : eq x y -> Compare lt eq x y
   | GT : lt y x -> Compare lt eq x y.
 
-Implicit Arguments LT [X lt eq x y].
-Implicit Arguments EQ [X lt eq x y].
-Implicit Arguments GT [X lt eq x y].
+Arguments LT [X lt eq x y] _.
+Arguments EQ [X lt eq x y] _.
+Arguments GT [X lt eq x y] _.
 
 Module Type MiniOrderedType.
 
diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v
index 62cce1d26..bac50fc45 100644
--- a/theories/ZArith/Int.v
+++ b/theories/ZArith/Int.v
@@ -27,7 +27,7 @@ Module Type Int.
   Parameter int : Set.
 
   Parameter i2z : int -> Z.
-  Arguments Scope i2z [ Int_scope ].
+  Arguments i2z _%I.
 
   Parameter _0 : int.
   Parameter _1 : int.
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index 86e9eb8ca..5a2c3cc32 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -111,7 +111,7 @@ Fixpoint Zlength_aux (acc:Z) (A:Type) (l:list A) : Z :=
   end.
 
 Definition Zlength := Zlength_aux 0.
-Implicit Arguments Zlength [A].
+Arguments Zlength [A] l.
 
 Section Zlength_properties.
 
@@ -146,6 +146,6 @@ Section Zlength_properties.
 
 End Zlength_properties.
 
-Implicit Arguments Zlength_correct [A].
-Implicit Arguments Zlength_cons [A].
-Implicit Arguments Zlength_nil_inv [A].
+Arguments Zlength_correct [A] l.
+Arguments Zlength_cons [A] x l.
+Arguments Zlength_nil_inv [A] l _.
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index e5a92024f..314f696a2 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -124,7 +124,7 @@ Proof.
   exact (Z_div_mod a b Hb).
 Qed.
 
-Implicit Arguments Zdiv_eucl_exist.
+Arguments Zdiv_eucl_exist : default implicits.
 
 
 (** Uniqueness theorems *)
@@ -679,7 +679,7 @@ Proof.
   rewrite Z.abs_neq; [ assumption | omega ].
 Qed.
 
-Implicit Arguments Zdiv_eucl_extended.
+Arguments Zdiv_eucl_extended : default implicits.
 
 (** * Division and modulo in Z agree with same in nat: *)