From 027fb68b3c9014f66a7e75255b5769f414d14655 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 7 Apr 2003 08:44:10 +0000
Subject: Espaces superflus

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

diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v
index 60befa9da9..8b209bde22 100644
--- a/theories/Reals/Rsyntax.v
+++ b/theories/Reals/Rsyntax.v
@@ -221,16 +221,16 @@ Notation "- x" := (Ropp x) (at level 0) : R_scope
 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).
-Notation "x  <=  y  <=  z" := (Rle x y)/\(Rle y z)
+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).
-Notation "x  <=  y  <  z"  := (Rle x y)/\(Rlt y z)
+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).
-Notation  "x  <  y  <  z"  := (Rlt x y)/\(Rlt y z)
+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).
-Notation  "x  <  y  <=  z" := (Rlt x y)/\(Rle y z)
+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).
 Notation "x <> y" := ~(eqT R x y) (at level 5) : R_scope.
-- 
cgit v1.2.3