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, 17 insertions, 19 deletions

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.