From ed06a90f16fcf7d45672bbddf42efe4cc0efd4d4 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Mon, 21 Nov 2011 17:03:52 +0000
Subject: 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
---
 theories/Program/Syntax.v | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'theories/Program/Syntax.v')

diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v
index a66e1284b9..61d389ed52 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.
-- 
cgit v1.2.3