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

10 files changed, 22 insertions, 22 deletions

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).