aboutsummaryrefslogtreecommitdiffstats
path: root/backend/CSE3.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/CSE3.v')
-rw-r--r--backend/CSE3.v2
1 files changed, 0 insertions, 2 deletions
diff --git a/backend/CSE3.v b/backend/CSE3.v
index 54a8a3bc..2f73a1a7 100644
--- a/backend/CSE3.v
+++ b/backend/CSE3.v
@@ -25,7 +25,6 @@ Record cse3params : Type :=
mkcse3params
{ cse3_conditions : bool;
cse3_operations : bool;
- cse3_loads : bool;
cse3_trivial_ops: bool;
}.
@@ -147,7 +146,6 @@ End PARAMS.
Definition cmdline_params (_ : unit) :=
{| cse3_conditions := Compopts.optim_CSE3_conditions tt;
cse3_operations := true;
- cse3_loads := true;
cse3_trivial_ops:= Compopts.optim_CSE3_trivial_ops tt |}.
Definition transf_program p := param_transf_program (cmdline_params tt) p.