Remplacement de Syntactic Definition par Notation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3267 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 13 insertions, 14 deletions

diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v
index ac3233704..6e9cbf062 100644
--- a/theories/Wellfounded/Disjoint_Union.v
+++ b/theories/Wellfounded/Disjoint_Union.v
@@ -19,7 +19,7 @@ Variable A,B:Set.
 Variable leA: A->A->Prop.
 Variable leB: B->B->Prop.
 
-Syntactic Definition Le_AsB := (le_AsB A B leA leB).
+Notation Le_AsB := (le_AsB A B leA leB).
 
 Lemma acc_A_sum: (x:A)(Acc A leA x)->(Acc A+B Le_AsB (inl A B x)).
 Proof.
diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v
index ad157ea9d..5c73cdae0 100644
--- a/theories/Wellfounded/Lexicographic_Exponentiation.v
+++ b/theories/Wellfounded/Lexicographic_Exponentiation.v
@@ -23,15 +23,15 @@ Section Wf_Lexicographic_Exponentiation.
 Variable A:Set.
 Variable leA: A->A->Prop.
 
-Syntactic Definition Power := (Pow A leA).
-Syntactic Definition Lex_Exp := (lex_exp A leA).
-Syntactic Definition ltl := (Ltl A leA).
-Syntactic Definition Descl := (Desc A leA).
+Notation Power := (Pow A leA).
+Notation Lex_Exp := (lex_exp A leA).
+Notation ltl := (Ltl A leA).
+Notation Descl := (Desc A leA).
 
-Syntactic Definition List := (list A).
-Syntactic Definition Nil := (nil A).
+Notation List := (list A).
+Notation Nil := (nil A).
 (* useless but symmetric *)
-Syntactic Definition Cons := (cons 1!A).
+Notation Cons := (cons 1!A).
 
 Syntax constr
   level 1:
diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v
index 3e8ba318a..39b00e676 100644
--- a/theories/Wellfounded/Lexicographic_Product.v
+++ b/theories/Wellfounded/Lexicographic_Product.v
@@ -23,8 +23,7 @@ Variable B:A->Set.
 Variable leA: A->A->Prop.
 Variable leB: (x:A)(B x)->(B x)->Prop.
 
-
-Syntactic Definition LexProd := (lexprod A B leA leB).
+Notation LexProd := (lexprod A B leA leB).
 
 Hints Resolve t_step Acc_clos_trans wf_clos_trans.
 
@@ -86,7 +85,7 @@ Section Wf_Symmetric_Product.
   Variable leA: A->A->Prop.
   Variable leB: B->B->Prop.
 
-  Syntactic Definition Symprod := (symprod A B leA leB).
+  Notation Symprod := (symprod A B leA leB).
 
 (*i
   Local sig_prod:=
@@ -135,7 +134,7 @@ Section Swap.
   Variable A:Set.
   Variable R:A->A->Prop.
 
-  Syntactic Definition SwapProd :=(swapprod A R).
+  Notation SwapProd :=(swapprod A R).
 
 
   Lemma swap_Acc: (x,y:A)(Acc A*A SwapProd (x,y))->(Acc A*A SwapProd (y,x)).
diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v
index 1cb9848f6..1198c1d47 100644
--- a/theories/Wellfounded/Transitive_Closure.v
+++ b/theories/Wellfounded/Transitive_Closure.v
@@ -17,7 +17,7 @@ Section Wf_Transitive_Closure.
   Variable A: Set.
   Variable R: (relation A).
 
-  Syntactic Definition trans_clos := (clos_trans A R).
+  Notation trans_clos := (clos_trans A R).
  
   Lemma incl_clos_trans: (inclusion A R trans_clos).
     Red;Auto with sets.
diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v
index 9c013bd11..084538d8c 100644
--- a/theories/Wellfounded/Union.v
+++ b/theories/Wellfounded/Union.v
@@ -18,7 +18,7 @@ Section WfUnion.
   Variable A: Set.
   Variable R1,R2: (relation A).
   
- Syntactic Definition Union := (union A R1 R2).
+ Notation Union := (union A R1 R2).
 
  Hints Resolve Acc_clos_trans wf_clos_trans.