aboutsummaryrefslogtreecommitdiff
path: root/src/Util/ZRange.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Util/ZRange.v')
-rw-r--r--src/Util/ZRange.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Util/ZRange.v b/src/Util/ZRange.v
index f68b3e5ff..7b9329dca 100644
--- a/src/Util/ZRange.v
+++ b/src/Util/ZRange.v
@@ -47,6 +47,6 @@ Defined.
Module Export Notations.
Delimit Scope zrange_scope with zrange.
- Notation "b[ l ~> u ]" := {| lower := l ; upper := u |}
- (format "b[ l ~> u ]") : zrange_scope.
+ Notation "r[ l ~> u ]" := {| lower := l ; upper := u |}
+ (format "r[ l ~> u ]") : zrange_scope.
End Notations.