diff options
Diffstat (limited to 'backend/LICM.v')
| -rw-r--r-- | backend/LICM.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/backend/LICM.v b/backend/LICM.v index 1b5334ba..d45eef43 100644 --- a/backend/LICM.v +++ b/backend/LICM.v @@ -6,4 +6,7 @@ Require Inject. Definition gen_injections (f : function) (max_pc : node) (max_reg : reg): PTree.t (list Inject.inj_instr) := PTree.empty (list Inject.inj_instr). -Definition transf_program := Inject.transf_program gen_injections. +Opaque gen_injections. + +Definition transf_program : program -> res program := + Inject.transf_program gen_injections. |