aboutsummaryrefslogtreecommitdiff
path: root/src/Util
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2018-11-01 16:51:31 -0400
committerGravatar Jason Gross <jgross@mit.edu>2018-11-01 16:51:31 -0400
commitdccf77649072d659541f2cacd6d3f8a0e8fb23dc (patch)
treed5731292384506650969185ef2085a146f2ca312 /src/Util
parenta9cbd7b66e2d8e6456c8f788b4587dec2e2e3cee (diff)
Make pairs work in Z_cast2
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.