From f5aad1456221340f4442268afca5ea06d41eef10 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 17 Apr 2003 16:34:22 +0000
Subject: <> maintenant standard

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3942 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Reals/Rsyntax.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories')

diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v
index 14cb0c8084..4733ad3cb8 100644
--- a/theories/Reals/Rsyntax.v
+++ b/theories/Reals/Rsyntax.v
@@ -230,7 +230,7 @@ Notation "x < y < z" := (Rlt x y)/\(Rlt 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.
+(*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