aboutsummaryrefslogtreecommitdiff
path: root/theories/Structures
diff options
context:
space:
mode:
authorJason Gross2020-03-23 15:53:26 -0400
committerJason Gross2020-03-23 15:55:40 -0400
commit528dd28a48dd7b1898212e2aae9b43bb19fb91cc (patch)
treec797790a1aa47c14286b92a4dca0526c0262fc35 /theories/Structures
parentb079040702d34ab06a0b1da2893d739e04477b78 (diff)
Fix levels of `<=?` and `<?` in the stdlib
They were defined at level 70, no associativity in all but three places, where they were instead declared at level 35. Fixes #11890
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).