diff options
Diffstat (limited to 'mppa_k1c/Asmgen.v')
| -rw-r--r-- | mppa_k1c/Asmgen.v | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v index 46714496..58e80be1 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -19,16 +19,13 @@ Require Import Integers. Require Import Mach Asm Asmblock Asmblockgen Machblockgen. Require Import PostpassScheduling. Require Import Errors. -Require Import Compopts. Local Open Scope error_monad_scope. Definition transf_program (p: Mach.program) : res Asm.program := let mbp := Machblockgen.transf_program p in do abp <- Asmblockgen.transf_program mbp; - do abp' <- if Compopts.optim_postpass tt - then PostpassScheduling.transf_program abp - else OK abp; + do abp' <- PostpassScheduling.transf_program abp; OK (Asm.transf_program abp'). Definition transf_function (f: Mach.function) : res Asm.function := |