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

6 files changed, 13 insertions, 13 deletions

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