aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Compilers/CommonSubexpressionElimination.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Compilers/CommonSubexpressionElimination.v b/src/Compilers/CommonSubexpressionElimination.v
index c1ac37b62..c3937562a 100644
--- a/src/Compilers/CommonSubexpressionElimination.v
+++ b/src/Compilers/CommonSubexpressionElimination.v
@@ -146,7 +146,7 @@ Section symbolic.
| None => (symbolize_var xs tx, None)
end in
match sv with
- | Some v => @csef _ (eC (symbolicify_smart_var v sx)) xs
+ | Some v => @csef _ (eC (symbolicify_smart_var v sx)) (extendb xs sx v)
| None
=> LetIn ex' (fun x => let sx' := symbolicify_smart_var x sx in
@csef _ (eC sx') (extendb xs sx x))