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

2 files changed, 10 insertions, 10 deletions

diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index 5293a66cb..7cef5c5ad 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -17,7 +17,7 @@
 
 (** The polymorphic identity function is defined in [Datatypes]. *)
 
-Implicit Arguments id [[A]].
+Arguments id {A} x.
 
 (** Function composition. *)
 
@@ -53,5 +53,5 @@ Definition apply {A B} (f : A -> B) (x : A) := f x.
 
 (** Curryfication of [prod] is defined in [Logic.Datatypes]. *)
 
-Implicit Arguments prod_curry [[A] [B] [C]].
-Implicit Arguments prod_uncurry [[A] [B] [C]].
+Arguments prod_curry   {A B C} f p.
+Arguments prod_uncurry {A B C} f x y.
diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v
index a66e1284b..61d389ed5 100644
--- a/theories/Program/Syntax.v
+++ b/theories/Program/Syntax.v
@@ -18,15 +18,15 @@ Notation " () " := tt.
 
 (** Set maximally inserted implicit arguments for standard definitions. *)
 
-Implicit Arguments Some [[A]].
-Implicit Arguments None [[A]].
+Arguments Some {A} _.
+Arguments None {A}.
 
-Implicit Arguments pair [[A] [B]].
-Implicit Arguments fst [[A] [B]].
-Implicit Arguments snd [[A] [B]].
+Arguments pair {A B} _ _.
+Arguments fst {A B} _.
+Arguments snd {A B} _.
 
-Implicit Arguments nil [[A]].
-Implicit Arguments cons [[A]].
+Arguments nil {A}.
+Arguments cons {A} _ _.
 
 Require List.
 Export List.ListNotations.