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, 26 insertions, 26 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index bab764bcbf..41f6b70b2b 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -137,7 +137,7 @@ Inductive nat : Set :=
 
 Delimit Scope nat_scope with nat.
 Bind Scope nat_scope with nat.
-Arguments Scope S [nat_scope].
+Arguments S _%nat.
 
 
 (********************************************************************)
@@ -149,7 +149,7 @@ Inductive option (A:Type) : Type :=
   | Some : A -> option A
   | None : option A.
 
-Implicit Arguments None [A].
+Arguments None [A].
 
 Definition option_map (A B:Type) (f:A->B) o :=
   match o with
@@ -165,8 +165,8 @@ Inductive sum (A B:Type) : Type :=
 
 Notation "x + y" := (sum x y) : type_scope.
 
-Implicit Arguments inl [[A] [B]] [A].
-Implicit Arguments inr [[A] [B]] [B].
+Arguments inl {A B} _ , [A] B _.
+Arguments inr {A B} _ , A [B] _.
 
 (** [prod A B], written [A * B], is the product of [A] and [B];
     the pair [pair A B a b] of [a] and [b] is abbreviated [(a,b)] *)
@@ -179,7 +179,7 @@ Add Printing Let prod.
 Notation "x * y" := (prod x y) : type_scope.
 Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
 
-Implicit Arguments pair [[A] [B]].
+Arguments pair {A B} _ _.
 
 Section projections.
   Variables A B : Type.
@@ -221,7 +221,7 @@ Inductive list (A : Type) : Type :=
  | nil : list A
  | cons : A -> list A -> list A.
 
-Implicit Arguments nil [A].
+Arguments nil [A].
 Infix "::" := cons (at level 60, right associativity) : list_scope.
 Delimit Scope list_scope with list.
 Bind Scope list_scope with list.
@@ -330,9 +330,9 @@ Inductive identity (A:Type) (a:A) : A -> Type :=
   identity_refl : identity a a.
 Hint Resolve identity_refl: core.
 
-Implicit Arguments identity_ind [A].
-Implicit Arguments identity_rec [A].
-Implicit Arguments identity_rect [A].
+Arguments identity_ind [A] a P f y i.
+Arguments identity_rec [A] a P f y i.
+Arguments identity_rect [A] a P f y i.
 
 (** Identity type *)
 
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index b9e22f15ed..d1eabcabf1 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -62,8 +62,8 @@ Inductive or (A B:Prop) : Prop :=
 
 where "A \/ B" := (or A B) : type_scope.
 
-Implicit Arguments or_introl [A B] [A].
-Implicit Arguments or_intror [A B] [B].
+Arguments or_introl [A B] _, [A] B _.
+Arguments or_intror [A B] _, A [B] _.
 
 (** [iff A B], written [A <-> B], expresses the equivalence of [A] and [B] *)
 
@@ -270,12 +270,12 @@ Notation "x = y" := (x = y :>_) : type_scope.
 Notation "x <> y  :> T" := (~ x = y :>T) : type_scope.
 Notation "x <> y" := (x <> y :>_) : type_scope.
 
-Implicit Arguments eq [[A]].
-Implicit Arguments eq_refl [[A] [x]] [A].
+Arguments eq {A} x _.
+Arguments eq_refl {A x} , [A] x.
 
-Implicit Arguments eq_ind [A].
-Implicit Arguments eq_rec [A].
-Implicit Arguments eq_rect [A].
+Arguments eq_ind [A] x P _ y _.
+Arguments eq_rec [A] x P _ y _.
+Arguments eq_rect [A] x P _ y _.
 
 Hint Resolve I conj or_introl or_intror eq_refl: core.
 Hint Resolve ex_intro ex_intro2: core.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 12ac08ff0c..637994b2b8 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -38,10 +38,10 @@ Inductive sigT2 (A:Type) (P Q:A -> Type) : Type :=
 
 (* Notations *)
 
-Arguments Scope sig [type_scope type_scope].
-Arguments Scope sig2 [type_scope type_scope type_scope].
-Arguments Scope sigT [type_scope type_scope].
-Arguments Scope sigT2 [type_scope type_scope type_scope].
+Arguments sig (A P)%type.
+Arguments sig2 (A P Q)%type.
+Arguments sigT (A P)%type.
+Arguments sigT2 (A P Q)%type.
 
 Notation "{ x  |  P }" := (sig (fun x => P)) : type_scope.
 Notation "{ x  |  P  & Q }" := (sig2 (fun x => P) (fun x => Q)) : type_scope.
@@ -126,8 +126,8 @@ Inductive sumbool (A B:Prop) : Set :=
 
 Add Printing If sumbool.
 
-Implicit Arguments left [[A] [B]] [A].
-Implicit Arguments right [[A] [B]] [B].
+Arguments left {A B} _, [A] B _.
+Arguments right {A B} _ , A [B] _.
 
 (** [sumor] is an option type equipped with the justification of why
     it may not be a regular value *)
@@ -139,8 +139,8 @@ Inductive sumor (A:Type) (B:Prop) : Type :=
 
 Add Printing If sumor.
 
-Implicit Arguments inleft [[A] [B]] [A].
-Implicit Arguments inright [[A] [B]] [B].
+Arguments inleft {A B} _ , [A] B _.
+Arguments inright {A B} _ , A [B] _.
 
 (** Various forms of the axiom of choice for specifications *)
 
@@ -208,11 +208,11 @@ Definition Exc := option.
 Definition value := Some.
 Definition error := @None.
 
-Implicit Arguments error [A].
+Arguments error [A].
 
 Definition except := False_rec. (* for compatibility with previous versions *)
 
-Implicit Arguments except [P].
+Arguments except [P] _.
 
 Theorem absurd_set : forall (A:Prop) (C:Set), A -> ~ A -> C.
 Proof.