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

3 files changed, 10 insertions, 10 deletions

diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index b06e42ca24..7f205b3882 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 668a111231..3ea3d5fd5b 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 aed96a831a..4717d0b233 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.