Make pairs work in Z_cast2

2 files changed, 6 insertions, 0 deletions

diff --git a/src/Experiments/NewPipeline/Language.v b/src/Experiments/NewPipeline/Language.v
index 07b416f54..a0fc9ade5 100644
--- a/src/Experiments/NewPipeline/Language.v
+++ b/src/Experiments/NewPipeline/Language.v
@@ -887,6 +887,8 @@ Module Compilers.
         | fancy_addm : ident (Z * Z * Z -> Z)
         .
 
+        Global Arguments Z_cast2 _%zrange_scope.
+
         Definition to_fancy {s d : base.type} (idc : ident (s -> d)) : option (fancy.ident s d)
           := match idc in ident t return option match t with
                                                 | type.base s -> type.base d => fancy.ident s d
@@ -1296,6 +1298,8 @@ Module Compilers.
       Notation "x 'mod' y" := (#Z_modulo @ x @ y)%expr : expr_scope.
       Notation "- x" := (#Z_opp @ x)%expr : expr_scope.
       Global Arguments gen_interp _ _ !_.
+
+      Global Arguments ident.Z_cast2 _%zrange_scope.
     End Notations.
   End ident.
   Export ident.Notations.
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.