diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-14 19:36:17 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-14 19:36:33 -0400 |
| commit | 62058145e881e9f96da18ee970182a95af957882 (patch) | |
| tree | 8f6e737c44750ad776918a10c0fcfc7cea77a41a /src/Specific | |
| parent | aa0052b9469c876947cbe7ed007ae8113b711fdc (diff) | |
Add support for cse-modulo-normalization
Diffstat (limited to 'src/Specific')
| -rw-r--r-- | src/Specific/FancyMachine256/Core.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Specific/FancyMachine256/Core.v b/src/Specific/FancyMachine256/Core.v index adb29e81f..6fe27b2e4 100644 --- a/src/Specific/FancyMachine256/Core.v +++ b/src/Specific/FancyMachine256/Core.v @@ -108,7 +108,7 @@ Section reflection. | OPaddm => SOPaddm end. - Definition CSE {t} e := @CSE base_type op_code base_type_beq op_code_beq internal_base_type_dec_bl op symbolicify_op 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) t e (fun _ => nil). Inductive inline_option := opt_inline | opt_default | opt_noinline. |