diff options
| -rw-r--r-- | theories/Reals/Rsyntax.v | 8 |
1 files 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. |