aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers/Z/Bounds/Pipeline/Definition.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Compilers/Z/Bounds/Pipeline/Definition.v')
-rw-r--r--src/Compilers/Z/Bounds/Pipeline/Definition.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/src/Compilers/Z/Bounds/Pipeline/Definition.v b/src/Compilers/Z/Bounds/Pipeline/Definition.v
index e5503511d..7d9061cad 100644
--- a/src/Compilers/Z/Bounds/Pipeline/Definition.v
+++ b/src/Compilers/Z/Bounds/Pipeline/Definition.v
@@ -81,7 +81,6 @@ Record PipelineOptions :=
{
anf : with_default bool false;
adc_fusion : with_default bool true;
- rename_binders : with_default bool false;
}.
Definition default_PipelineOptions := {| anf := _ |}.