aboutsummaryrefslogtreecommitdiff
path: root/theories/Structures
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Structures')
-rw-r--r--theories/Structures/Orders.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v
index 6a0e7397eb..94938c1d4d 100644
--- a/theories/Structures/Orders.v
+++ b/theories/Structures/Orders.v
@@ -192,11 +192,11 @@ Module Type HasLtb (Import T:Typ).
End HasLtb.
Module Type LebNotation (T:Typ)(E:HasLeb T).
- Infix "<=?" := E.leb (at level 35).
+ Infix "<=?" := E.leb (at level 70, no associativity).
End LebNotation.
Module Type LtbNotation (T:Typ)(E:HasLtb T).
- Infix "<?" := E.ltb (at level 35).
+ Infix "<?" := E.ltb (at level 70, no associativity).
End LtbNotation.
Module Type LebSpec (T:Typ)(X:HasLe T)(Y:HasLeb T).