aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments/NewPipeline/Toplevel1.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Experiments/NewPipeline/Toplevel1.v')
-rw-r--r--src/Experiments/NewPipeline/Toplevel1.v3
1 files changed, 1 insertions, 2 deletions
diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v
index 390683b93..b1bf23019 100644
--- a/src/Experiments/NewPipeline/Toplevel1.v
+++ b/src/Experiments/NewPipeline/Toplevel1.v
@@ -714,7 +714,6 @@ Module Pipeline.
let E := PartialEvaluate E in
let E := RewriteAndEliminateDeadAndInline (RewriteRules.RewriteArith 0) with_dead_code_elimination with_subst01 E in
let E := RewriteRules.RewriteArith (2^8) E in (* reassociate small consts *)
- let E := RewriteAndEliminateDeadAndInline RewriteRules.RewriteArithWithCasts with_dead_code_elimination with_subst01 E in
let E := match translate_to_fancy with
| Some {| invert_low := invert_low ; invert_high := invert_high |} => RewriteRules.RewriteToFancy invert_low invert_high E
| None => E
@@ -724,7 +723,7 @@ Module Pipeline.
let E' := CheckedPartialEvaluateWithBounds relax_zrange E arg_bounds out_bounds in
match E' with
| inl E
- => (*let E := RewriteAndEliminateDeadAndInline RewriteRules.RewriteArithWithCasts with_dead_code_elimination with_subst01 E in*)
+ => let E := RewriteAndEliminateDeadAndInline RewriteRules.RewriteArithWithCasts with_dead_code_elimination with_subst01 E in
let E := match translate_to_fancy with
| Some {| invert_low := invert_low ; invert_high := invert_high |} => RewriteRules.RewriteToFancyWithCasts invert_low invert_high E
| None => E