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

7 files changed, 46 insertions, 46 deletions

diff --git a/plugins/dp/test2.v b/plugins/dp/test2.v
index 0940b1352..ce6600520 100644
--- a/plugins/dp/test2.v
+++ b/plugins/dp/test2.v
@@ -73,7 +73,7 @@ zenon.
 Inductive IN (A:Set) : A -> list A -> Prop :=
   | IN1 : forall x l, IN A x (x::l)
   | IN2: forall x l, IN A x l -> forall y, IN A x (y::l).
-Implicit Arguments IN [A].
+Arguments IN [A] _ _.
 
 Goal forall x, forall (l:list nat), IN x l -> IN x (1%nat::l).
   zenon.
diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index 7b4fdb089..4af650861 100644
--- a/plugins/micromega/RingMicromega.v
+++ b/plugins/micromega/RingMicromega.v
@@ -308,7 +308,7 @@ Definition map_option (A B:Type) (f : A -> option B) (o : option A) : option B :
     | Some x => f x
   end.
 
-Implicit Arguments map_option [A B].
+Arguments map_option [A B] f o.
 
 Definition map_option2 (A B C : Type) (f : A -> B -> option C)
   (o: option A) (o': option B) : option C :=
@@ -318,7 +318,7 @@ Definition map_option2 (A B C : Type) (f : A -> B -> option C)
     | Some x , Some x' => f x x'
   end.
 
-Implicit Arguments map_option2 [A B C].
+Arguments map_option2 [A B C] f o o'.
 
 Definition Rops_wd := mk_reqe rplus rtimes ropp req
                        sor.(SORplus_wd)
@@ -1034,4 +1034,4 @@ End Micromega.
 
 (* Local Variables: *)
 (* coding: utf-8 *)
-(* End: *)
\ No newline at end of file
+(* End: *)
diff --git a/plugins/ring/Ring_normalize.v b/plugins/ring/Ring_normalize.v
index e499f2220..c6dff3e00 100644
--- a/plugins/ring/Ring_normalize.v
+++ b/plugins/ring/Ring_normalize.v
@@ -746,11 +746,11 @@ Qed.
 (* End properties. *)
 End semi_rings.
 
-Implicit Arguments Cons_varlist.
-Implicit Arguments Cons_monom.
-Implicit Arguments SPconst.
-Implicit Arguments SPplus.
-Implicit Arguments SPmult.
+Arguments Cons_varlist : default implicits.
+Arguments Cons_monom : default implicits.
+Arguments SPconst : default implicits.
+Arguments SPplus : default implicits.
+Arguments SPmult : default implicits.
 
 Section rings.
 
diff --git a/plugins/ring/Setoid_ring_normalize.v b/plugins/ring/Setoid_ring_normalize.v
index 41190e8d9..ad75a8a4d 100644
--- a/plugins/ring/Setoid_ring_normalize.v
+++ b/plugins/ring/Setoid_ring_normalize.v
@@ -1011,11 +1011,11 @@ Qed.
 
 End semi_setoid_rings.
 
-Implicit Arguments Cons_varlist.
-Implicit Arguments Cons_monom.
-Implicit Arguments SetSPconst.
-Implicit Arguments SetSPplus.
-Implicit Arguments SetSPmult.
+Arguments Cons_varlist : default implicits.
+Arguments Cons_monom : default implicits.
+Arguments SetSPconst : default implicits.
+Arguments SetSPplus : default implicits.
+Arguments SetSPmult : default implicits.
 
 
 
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index f311d2447..56ae921ed 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -868,11 +868,11 @@ Inductive term : Set :=
   | Tvar : nat -> term.
 
 Delimit Scope romega_scope with term.
-Arguments Scope Tint [Int_scope].
-Arguments Scope Tplus [romega_scope romega_scope].
-Arguments Scope Tmult [romega_scope romega_scope].
-Arguments Scope Tminus [romega_scope romega_scope].
-Arguments Scope Topp [romega_scope romega_scope].
+Arguments Tint _%I.
+Arguments Tplus (_ _)%term.
+Arguments Tmult (_ _)%term.
+Arguments Tminus (_ _)%term.
+Arguments Topp _%term.
 
 Infix "+" := Tplus : romega_scope.
 Infix "*" := Tmult : romega_scope.
diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v
index b34cf338b..77f8f8345 100644
--- a/plugins/rtauto/Bintree.v
+++ b/plugins/rtauto/Bintree.v
@@ -34,7 +34,7 @@ match n with O => Some x
 | S m => Lget A m q
 end end .
 
-Implicit Arguments Lget [A].
+Arguments Lget [A] n l.
 
 Lemma map_app : forall (A B:Set) (f:A -> B) l m,
 List.map  f (l ++ m) = List.map  f  l ++ List.map  f  m.
@@ -288,34 +288,34 @@ Qed.
 
 End Store.
 
-Implicit Arguments PNone [A].
-Implicit Arguments PSome [A].
+Arguments PNone [A].
+Arguments PSome [A] _.
 
-Implicit Arguments Tempty [A].
-Implicit Arguments Branch0 [A].
-Implicit Arguments Branch1 [A].
+Arguments Tempty [A].
+Arguments Branch0 [A] _ _.
+Arguments Branch1 [A] _ _ _.
 
-Implicit Arguments Tget [A].
-Implicit Arguments Tadd [A].
+Arguments Tget [A] p T.
+Arguments Tadd [A] p a T.
 
-Implicit Arguments Tget_Tempty [A].
-Implicit Arguments Tget_Tadd [A].
+Arguments Tget_Tempty [A] p.
+Arguments Tget_Tadd [A] i j a T.
 
-Implicit Arguments mkStore [A].
-Implicit Arguments index [A].
-Implicit Arguments contents [A].
+Arguments mkStore [A] index contents.
+Arguments index [A] s.
+Arguments contents [A] s.
 
-Implicit Arguments empty [A].
-Implicit Arguments get [A].
-Implicit Arguments push [A].
+Arguments empty [A].
+Arguments get [A] i S.
+Arguments push [A] a S.
 
-Implicit Arguments get_empty [A].
-Implicit Arguments get_push_Full [A].
+Arguments get_empty [A] i.
+Arguments get_push_Full [A] i a S _.
 
-Implicit Arguments Full [A].
-Implicit Arguments F_empty [A].
-Implicit Arguments F_push [A].
-Implicit Arguments In [A].
+Arguments Full [A] _.
+Arguments F_empty [A].
+Arguments F_push [A] a S _.
+Arguments In [A] x S F.
 
 Section Map.
 
@@ -367,8 +367,8 @@ Defined.
 
 End Map.
 
-Implicit Arguments Tmap [A B].
-Implicit Arguments map [A B].
-Implicit Arguments Full_map [A B f].
+Arguments Tmap [A B] f T.
+Arguments map [A B] f S.
+Arguments Full_map [A B f] S _.
 
 Notation "hyps \ A" := (push A hyps) (at level 72,left associativity).
diff --git a/plugins/rtauto/Rtauto.v b/plugins/rtauto/Rtauto.v
index 8b5e42447..9cae7a44e 100644
--- a/plugins/rtauto/Rtauto.v
+++ b/plugins/rtauto/Rtauto.v
@@ -73,7 +73,7 @@ case_eq (form_eq p1 q1);clean.
 intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence.
 Qed.
 
-Implicit Arguments form_eq_refl [p q].
+Arguments form_eq_refl [p q] _.
 
 Section with_env.
 
@@ -161,7 +161,7 @@ intros hyps F p g e; apply project_In.
 apply get_In with p;assumption.
 Qed.
 
-Implicit Arguments project [hyps p g].
+Arguments project [hyps] F [p g] _.
 
 Inductive proof:Set :=
   Ax : positive -> proof