diff options
Diffstat (limited to 'src/RewriterRules.v')
| -rw-r--r-- | src/RewriterRules.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/RewriterRules.v b/src/RewriterRules.v index 8f23c1793..08a4e8d1f 100644 --- a/src/RewriterRules.v +++ b/src/RewriterRules.v @@ -318,6 +318,9 @@ Definition arith_rewrite_rulesT (max_const_val : Z) : list (bool * Prop) ; (forall s c y x, Z.add_with_get_carry_full s (- c) x (- y) = dlet vb := Z.sub_with_get_borrow_full s c x y in (fst vb, - snd vb)) + ; (forall b x, (* inline negation when the rewriter wouldn't already inline it *) + ident.gets_inlined b x = false + -> -x = dlet v := x in -v) ] ]. |