From d93a43901ff6a4bd264383df486f2dd1387157e6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 29 May 2003 22:11:18 +0000
Subject: niveau 49 devient next

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4091 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Reals/Rsyntax.v | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v
index a008cd06ec..60a205cfd9 100644
--- a/theories/Reals/Rsyntax.v
+++ b/theories/Reals/Rsyntax.v
@@ -222,19 +222,19 @@ Notation "- x" := (Ropp x) (at level 0) : R_scope
   V8only (at level 40, left associativity).
 Notation "x == y == z" := (eqT R x y)/\(eqT R y z)
   (at level 5, y at level 4, no associtivity): R_scope
-  V8only (at level 50, y at level 49, no associativity).
+  V8only (at level 50, y at next level, no associativity).
 Notation "x <= y <= z" := (Rle x y)/\(Rle y z)
   (at level 5, y at level 4) : R_scope
-  V8only (at level 50, y at level 49, no associativity).
+  V8only (at level 50, y at next level, no associativity).
 Notation "x <= y < z" := (Rle x y)/\(Rlt y z)
   (at level 5, y at level 4) : R_scope
-  V8only (at level 50, y at level 49, no associativity).
+  V8only (at level 50, y at next level, no associativity).
 Notation "x < y < z" := (Rlt x y)/\(Rlt y z)
   (at level 5, y at level 4) : R_scope
-  V8only (at level 50, y at level 49, no associativity).
+  V8only (at level 50, y at next level, no associativity).
 Notation "x < y <= z" := (Rlt x y)/\(Rle y z)
   (at level 5, y at level 4) : R_scope
-  V8only (at level 50, y at level 49, no associativity).
+  V8only (at level 50, y at next level, no associativity).
 (*Notation "x <> y" := ~(eqT R x y) (at level 5) : R_scope.*)
 Notation "/ x" := (Rinv x) (at level 0): R_scope
   V8only (at level 30, left associativity).
-- 
cgit v1.2.3