diff options
| author | herbelin | 2003-04-17 16:34:22 +0000 |
|---|---|---|
| committer | herbelin | 2003-04-17 16:34:22 +0000 |
| commit | f5aad1456221340f4442268afca5ea06d41eef10 (patch) | |
| tree | 8427b2f2369695e54ee61c53c94dfcbccbce07d4 | |
| parent | ce8a3c9ab2b1be834911f9a717e935b8a2cebd0c (diff) | |
<> maintenant standard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3942 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | theories/Reals/Rsyntax.v | 2 |
1 files changed, 1 insertions, 1 deletions
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). |