From a9cbd7b66e2d8e6456c8f788b4587dec2e2e3cee Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 1 Nov 2018 16:17:18 -0400 Subject: Export ZRange operation notations --- src/Util/ZRange/Operations.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'src/Util/ZRange') 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. -- cgit v1.2.3