diff options
Diffstat (limited to 'src/Rewriter.v')
| -rw-r--r-- | src/Rewriter.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Rewriter.v b/src/Rewriter.v index 8bbf13173..fb14b31f0 100644 --- a/src/Rewriter.v +++ b/src/Rewriter.v @@ -1793,6 +1793,13 @@ Module Compilers. ; make_rewriteo (??') (fun r v => ##(lower r) when lower r =? upper r) ; make_rewriteo + (#?ℤ +' ??') + (fun rp z rv v => cst rv v when (z =? 0) && (ZRange.normalize rv <=? ZRange.normalize rp)%zrange) + ; make_rewriteo + (??' +' #?ℤ ) + (fun rp rv v z => cst rv v when (z =? 0) && (ZRange.normalize rv <=? ZRange.normalize rp)%zrange) + + ; make_rewriteo (#?ℤ - (-'??')) (fun z rnv rv v => cst rv v when (z =? 0) && (ZRange.normalize rv <=? -ZRange.normalize rnv)%zrange) ; make_rewriteo (#?ℤ - ?? ) (fun z v => -v when z =? 0) |