diff options
Diffstat (limited to 'src/Rewriter.v')
| -rw-r--r-- | src/Rewriter.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Rewriter.v b/src/Rewriter.v index 76071b866..8bbf13173 100644 --- a/src/Rewriter.v +++ b/src/Rewriter.v @@ -1790,6 +1790,8 @@ Module Compilers. := [make_rewrite (#(@pattern.ident.fst '1 '2) @ (??, ??)) (fun _ _ x y => x) ; make_rewrite (#(@pattern.ident.snd '1 '2) @ (??, ??)) (fun _ x _ y => y) + ; make_rewriteo (??') (fun r v => ##(lower r) when lower r =? upper r) + ; make_rewriteo (#?ℤ - (-'??')) (fun z rnv rv v => cst rv v when (z =? 0) && (ZRange.normalize rv <=? -ZRange.normalize rnv)%zrange) |