niveau 49 devient next

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

1 files changed, 7 insertions, 9 deletions

diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v
index cd116ecb0..180596d8d 100644
--- a/theories/ZArith/Zsyntax.v
+++ b/theories/ZArith/Zsyntax.v
@@ -225,7 +225,7 @@ Syntax constr
 ].
 
 (* For parsing/printing based on scopes *)
-V7only [
+V7only[
 Module Z_scope.
 ].
 
@@ -241,19 +241,19 @@ Infix NONA 5 ">"  Zgt  : Z_scope.
 Infix NONA 5 "?=" Zcompare : Z_scope.
 Notation "x <= y <= z" := (Zle x y)/\(Zle y z)
   (at level 5, y at level 4):Z_scope
-  V8only (at level 50, y at level 49).
+  V8only (at level 50, y at next level).
 Notation "x <= y < z"  := (Zle x y)/\(Zlt y z)
   (at level 5, y at level 4):Z_scope
-  V8only (at level 50, y at level 49).
+  V8only (at level 50, y at next level).
 Notation  "x < y < z"  := (Zlt x y)/\(Zlt y z)
   (at level 5, y at level 4):Z_scope
-  V8only (at level 50, y at level 49).
+  V8only (at level 50, y at next level).
 Notation  "x < y <= z" := (Zlt x y)/\(Zle y z)
   (at level 5, y at level 4):Z_scope
-  V8only (at level 50, y at level 49).
+  V8only (at level 50, y at next level).
 Notation  "x = y = z" := x=y/\y=z
   (at level 5, y at level 4) : Z_scope
-  V8only (at level 50, y at level 49).
+  V8only (at level 50, y at next level).
 
 (* Now a polymorphic notation
 Notation "x <> y" := ~(eq Z x y) (at level 5, no associativity) : Z_scope.
@@ -265,10 +265,9 @@ V7only[
 (* Overwrite the printing of "`x = y`" *)
 Syntax constr level 0:
   Zeq [ (eq Z $n1 $n2) ] -> [[<hov 0> $n1 [1 0] "= " $n2 ]].
-].
 
-V7only [
 Open Scope Z_scope.
+
 End Z_scope.
 ].
 
@@ -279,4 +278,3 @@ Delimits Scope Z_scope with Z.
 
 Arguments Scope POS [positive_scope].
 Arguments Scope NEG [positive_scope].
-