diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/Compilers/Z/ArithmeticSimplifier.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Compilers/Z/ArithmeticSimplifier.v b/src/Compilers/Z/ArithmeticSimplifier.v index 24072dc71..771a82de4 100644 --- a/src/Compilers/Z/ArithmeticSimplifier.v +++ b/src/Compilers/Z/ArithmeticSimplifier.v @@ -415,14 +415,14 @@ Section language. (Op (OpConst v) TT, Op (OpConst c) TT)%expr | Some (c, gen_expr x, y) => let y' := match y with - | const_of y => if (y <? 0)%Z + | const_of y => if (y <=? 0)%Z then Some (Op (OpConst (-y)) TT) else None | neg_expr y => Some y | gen_expr _ => None end in let c' := match c with - | const_of c => if (c <? 0)%Z + | const_of c => if (c <=? 0)%Z then Some (Op (OpConst (-c)) TT) else None | neg_expr c => Some c |