Remplacement de Syntactic Definition par Notation

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

8 files changed, 18 insertions, 19 deletions

diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v
index 0df34f422..f4eea6c2f 100644
--- a/contrib/romega/ReflOmegaCore.v
+++ b/contrib/romega/ReflOmegaCore.v
@@ -50,7 +50,7 @@ Inductive proposition : Set :=
 | NeqTerm: term -> term -> proposition.
 
 (* Définition des hypothèses *)
-Syntactic Definition hyps := (list proposition).      
+Notation hyps := (list proposition).      
 
 Definition absurd := (cons FalseTerm (nil proposition)).
 
@@ -413,7 +413,7 @@ Save.
 
 (* \subsubsection{Généralisation à des listes de buts (disjonctions)} *)
 
-Syntactic Definition lhyps := (list hyps).
+Notation lhyps := (list hyps).
 
 Fixpoint interp_list_hyps [env: (list Z); l : lhyps] : Prop :=
    Cases l of
@@ -1778,7 +1778,7 @@ Inductive t_omega : Set :=
  | O_NEGATE_CONTRADICT_INV : nat -> nat -> nat -> t_omega
  | O_STATE : Z -> step -> nat -> nat -> t_omega -> t_omega.
 
-Syntactic Definition singleton :=  [a: hyps] (cons a (nil hyps)).
+Notation singleton :=  [a: hyps] (cons a (nil hyps)).
 
 Fixpoint execute_omega [t: t_omega] : hyps -> lhyps := 
   [l : hyps] Cases t of
diff --git a/test-suite/modules/sub_objects.v b/test-suite/modules/sub_objects.v
index 73fd6f322..2dbac3407 100644
--- a/test-suite/modules/sub_objects.v
+++ b/test-suite/modules/sub_objects.v
@@ -14,7 +14,7 @@ Module M.
     Definition idid:=[A:Set][x:A](id x).
     Grammar constr constr8 := 
       not_eq [ "#"  constr7($b) ] -> [ (idid $b) ].
-    Syntactic Definition inc := (plus (S O)). 
+    Notation inc := (plus (S O)). 
   End N.
 
   Definition zero:=(N.idid O).
diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v
index 5dd687859..8d0dc0f5c 100644
--- a/test-suite/success/CasesDep.v
+++ b/test-suite/success/CasesDep.v
@@ -109,7 +109,7 @@ Definition Map_setoid := (Build_Setoid Map ext Equiv_map_eq).
 
 End Maps.
 
-Syntactic Definition ap := (explicit_ap ? ?). 
+Notation ap := (explicit_ap ? ?). 
 
 Grammar constr constr8 :=
   map_setoid [ constr7($c1) "=>" constr8($c2) ] 
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.