Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; améliorations diverses de l'affichage; affinement de la syntaxe et des options de Notation; branchement de Syntactic Definition sur Notation

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

2 files changed, 38 insertions, 22 deletions

diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v
index 6cc0d71c4e..77ecf144df 100644
--- a/theories/Reals/Rsyntax.v
+++ b/theories/Reals/Rsyntax.v
@@ -199,7 +199,7 @@ Syntax constr
 (* For parsing/printing based on scopes *)
 Module R_scope.
 
-Delimiters "'R:" R_scope "'".
+Delimits Scope R_scope with R.
 Infix NONA 5 "<=" Rle : R_scope.
 Infix NONA 5 "<"  Rlt : R_scope.
 Infix NONA 5 ">=" Rge : R_scope.
@@ -209,12 +209,17 @@ Infix 4 "-" Rminus : R_scope.
 Infix 3 "*" Rmult : R_scope.
 Infix LEFTA 3 "/" Rdiv : R_scope.
 Distfix 0 "- _" Ropp : R_scope.
-Notation NONA 5 "x == y == z" (eqT R x y)/\(eqT R y z) (y at level 4): R_scope.
-Notation NONA 5 "x <= y <= z" (Rle x y)/\(Rle y z) (y at level 4) : R_scope.
-Notation NONA 5 "x <= y <  z" (Rle x y)/\(Rlt y z) (y at level 4) : R_scope.
-Notation NONA 5 "x <  y <  z" (Rlt x y)/\(Rlt y z) (y at level 4) : R_scope.
-Notation NONA 5 "x <  y <= z" (Rlt x y)/\(Rle y z) (y at level 4) : R_scope.
-Notation NONA 5 "x <> y"  ~(eqT R x y) : R_scope.
+Notation "x == y == z" := (eqT R x y)/\(eqT R y z)
+  (at level 5, y at level 4): R_scope.
+Notation "x <= y <= z" := (Rle x y)/\(Rle y z)
+  (at level 5, y at level 4) : R_scope.
+Notation "x <= y < z"  := (Rle x y)/\(Rlt y z)
+  (at level 5, y at level 4) : R_scope.
+Notation  "x < y < z"  := (Rlt x y)/\(Rlt y z)
+  (at level 5, y at level 4) : R_scope.
+Notation  "x < y <= z" := (Rlt x y)/\(Rle y z)
+  (at level 5, y at level 4) : R_scope.
+Notation "x <> y" := ~(eqT R x y) (at level 5) : R_scope.
 Distfix 0 "/ _" Rinv : R_scope.
 
 (* Warning: this hides sum and prod and breaks sumor symbolic notation *)
diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v
index ef9647413d..760c1fc896 100644
--- a/theories/ZArith/Zsyntax.v
+++ b/theories/ZArith/Zsyntax.v
@@ -219,23 +219,34 @@ Syntax constr
 (* For parsing/printing based on scopes *)
 Module Z_scope.
 
-Delimiters "'Z:" Z_scope "'".
-Infix 4 "+" Zplus : Z_scope.
-Infix 4 "-" Zminus : Z_scope.
-Infix 3 "*" Zmult : Z_scope.
+(* Declare Scope positive_scope with Key P. *)
+
+Delimits Scope positive_scope with P.
+Delimits Scope Z_scope with Z.
+
+Infix LEFTA 4 "+" Zplus : Z_scope.
+Infix LEFTA 4 "-" Zminus : Z_scope.
+Infix LEFTA 3 "*" Zmult : Z_scope.
 Distfix 0 "- _" Zopp : Z_scope.
-Infix NONA 5 "<=" Zle : Z_scope.
-Infix NONA 5 "<"  Zlt : Z_scope.
-Infix NONA 5 ">=" Zge : Z_scope.
+Infix 5 "<=" Zle : Z_scope.
+Infix 5 "<"  Zlt : Z_scope.
+Infix 5 ">=" Zge : Z_scope.
 (*Infix NONA 5 ">"  Zgt : Z_scope. (* Conflicts with "<..>Cases ... " *) *)
-Infix NONA 5 "?=" Zcompare : Z_scope.
-Notation NONA 5 "x <= y <= z" (Zle x y)/\(Zle y z) (y at level 4) : Z_scope.
-Notation NONA 5 "x <= y <  z" (Zle x y)/\(Zlt y z) (y at level 4) : Z_scope.
-Notation NONA 5 "x <  y <  z" (Zlt x y)/\(Zlt y z) (y at level 4) : Z_scope.
-Notation NONA 5 "x <  y <= z" (Zlt x y)/\(Zle y z) (y at level 4) : Z_scope.
-Notation NONA 5 "x <> y"      ~(eq Z x y)          : Z_scope.
-(* Notation NONA 1 "| x |" (Zabs x) : Z_scope.(* "|" conflicts with THENS *)*)
-Notation NONA 1 "|| x ||" (Zabs x) : Z_scope.
+Infix 5 "?=" Zcompare : Z_scope.
+Notation "x <= y <= z" := (Zle x y)/\(Zle y z)
+  (at level 5, y at level 4):Z_scope.
+Notation "x <= y < z"  := (Zle x y)/\(Zlt y z)
+  (at level 5, y at level 4):Z_scope.
+Notation  "x < y < z"  := (Zlt x y)/\(Zlt y z)
+  (at level 5, y at level 4):Z_scope.
+Notation  "x < y <= z" := (Zlt x y)/\(Zle y z)
+  (at level 5, y at level 4):Z_scope.
+Notation  "x = y = z" := x=y/\y=z
+  (at level 5, y at level 4):Z_scope.
+
+Notation "x <> y" := ~(eq Z x y) (at level 5) : Z_scope.
+(* Notation "| x |" (Zabs x) : Z_scope.(* "|" conflicts with THENS *)*)
+Notation "|| x ||" := (Zabs x) (at level 1) : Z_scope.
 
 (* Warning: this hides sum and prod and breaks sumor symbolic notation *)
 Open Scope Z_scope.