From a3d40b88608b8b5e7e615346ea1c33198355cbbc Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 1 Apr 2020 14:45:25 +0200 Subject: clearer types --- backend/LICM.v | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'backend/LICM.v') 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. -- cgit