Add support for reifying `zrange` and `option`

This is needed to reify statements for the rewriter.

1 files changed, 14 insertions, 0 deletions

diff --git a/src/BoundsPipeline.v b/src/BoundsPipeline.v
index 1c6cec4c7..f0c161dc2 100644
--- a/src/BoundsPipeline.v
+++ b/src/BoundsPipeline.v
@@ -141,6 +141,7 @@ Module Pipeline.
            => fun 'tt 'tt => (false, nil, nil)
          | base.type.nat
          | base.type.bool
+         | base.type.zrange
            => fun _ _ => (false, nil, nil)
          | base.type.Z
            => fun a b
@@ -153,6 +154,19 @@ Module Pipeline.
                       then (false, nil, nil)
                       else (false, nil, ((a, b)::nil))
                  end
+         | base.type.option A
+           => fun a b
+              => match a, b with
+                 | None, None => (false, nil, nil)
+                 | Some _, None => (false, nil, nil)
+                 | None, Some _ => (true, nil, nil)
+                 | Some None, Some None
+                 | Some (Some _), Some None
+                 | Some None, Some (Some _)
+                   => (false, nil, nil)
+                 | Some (Some a), Some (Some b)
+                   => @find_too_loose_base_bounds A a b
+                 end
          | base.type.prod A B
            => fun '(ra, rb) '(ra', rb')
               => let '(b1, lens1, ls1) := @find_too_loose_base_bounds A ra ra' in