diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-11-01 16:17:18 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-11-01 16:17:18 -0400 |
| commit | a9cbd7b66e2d8e6456c8f788b4587dec2e2e3cee (patch) | |
| tree | 2c6ed1214a7440ecb63eb1c2b89a487349598338 /src/Util | |
| parent | 8dd2ff5ebfd6dd49da64e4707f98f55bf76e36a8 (diff) | |
Export ZRange operation notations
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. |