diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-14 21:51:50 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-14 21:51:50 -0400 |
| commit | 1b732bd5dd2cedb821345f5772842c0994237722 (patch) | |
| tree | b8e3181441a0eefc46ca68189d30fdd6db22dd7e /src/Specific | |
| parent | 0faedd6652a3d0c7c0f21b34761f494a310ea62b (diff) | |
Split off a-normal form from flattening
Now we can flatten let binders without putting operations in a-normal form
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 6fe27b2e4..517644572 100644 --- a/src/Specific/FancyMachine256/Core.v +++ b/src/Specific/FancyMachine256/Core.v @@ -157,7 +157,7 @@ Ltac base_reify_type T ::= Ltac Reify' e := Reify.Reify' base_type (@interp_base_type _) (@op _) e. Ltac Reify e := let v := Reify.Reify base_type (@interp_base_type _) (@op _) (@OPconst _) e in - constr:(Inline ((*CSE _*) (InlineConst (@is_const _) (Linearize v)))). + constr:(Inline ((*CSE _*) (InlineConst (@is_const _) (ANormal v)))). (*Ltac Reify_rhs := Reify.Reify_rhs base_type (interp_base_type _) op (interp_op _).*) (** ** Raw Syntax Trees *) |