diff options
Diffstat (limited to 'src/Util')
| -rw-r--r-- | src/Util/ZRange/Operations.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/Util/ZRange/Operations.v b/src/Util/ZRange/Operations.v index 1497cb1ab..f0bdb276e 100644 --- a/src/Util/ZRange/Operations.v +++ b/src/Util/ZRange/Operations.v @@ -189,7 +189,7 @@ Module ZRange. Notation land := land_bounds. Notation lor := lor_bounds. - Module ZRangeNotations. + Module Export ZRangeNotations. Notation "- x" := (opp x) : zrange_scope. Infix "+" := add : zrange_scope. Infix "-" := sub : zrange_scope. @@ -200,3 +200,5 @@ Module ZRange. Infix "&'" := land : zrange_scope. End ZRangeNotations. End ZRange. + +Export ZRange.ZRangeNotations. |