CSE without inlining arithmetic expressions

This takes care of most of #158.  The remaining bits are reworking the
Wf and interpretation lemmas to actually work.  (The former needs a only
bit of rethinking and rephrasing to handle the fact that sometimes we
change the stored symbolic expression from a complicated one to a fresh
variable, while the latter needs major surgery, which Adam tells me is
easy, and this is a note that when I come back to it, I should look at
the email thread with Adam about CSE from last summer.)

1 files changed, 1 insertions, 1 deletions

diff --git a/src/Compilers/TestCase.v b/src/Compilers/TestCase.v
index a7fd81328..36774e4e3 100644
--- a/src/Compilers/TestCase.v
+++ b/src/Compilers/TestCase.v
@@ -187,7 +187,7 @@ Section cse.
        | Mul => SMul
        | Sub => SSub
        end.
-  Definition CSE {t} e := @CSE base_type op_code base_type_beq op_code_beq internal_base_type_dec_bl op symbolicify_op (fun _ x => x) t e (fun _ => nil).
+  Definition CSE {t} e := @CSE base_type op_code base_type_beq op_code_beq internal_base_type_dec_bl op symbolicify_op (fun _ x => x) true t e (fun _ => nil).
 End cse.
 
 Definition example_expr_simplified := Eval vm_compute in InlineConst is_const (ANormal example_expr).