aboutsummaryrefslogtreecommitdiff
path: root/src/Util
diff options
context:
space:
mode:
Diffstat (limited to 'src/Util')
-rw-r--r--src/Util/ZRange/Operations.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Util/ZRange/Operations.v b/src/Util/ZRange/Operations.v
index f0bdb276e..a0cf38f42 100644
--- a/src/Util/ZRange/Operations.v
+++ b/src/Util/ZRange/Operations.v
@@ -198,6 +198,8 @@ Module ZRange.
Infix ">>" := shiftr : zrange_scope.
Infix "<<" := shiftl : zrange_scope.
Infix "&'" := land : zrange_scope.
+ (* enable pairing to show up in arguments bound to zrange_scope *)
+ Notation "( x , y , .. , z )" := (pair .. (pair x%zrange y%zrange) .. z%zrange) : zrange_scope.
End ZRangeNotations.
End ZRange.