diff options
Diffstat (limited to 'mppa_k1c/Asmgen.v')
| -rw-r--r-- | mppa_k1c/Asmgen.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v index c3588871..8875a4ac 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -19,10 +19,11 @@ Require Import Integers. Require Import Mach Asm Asmblock Asmblockgen Machblockgen. Require Import PostpassScheduling. Require Import Errors String. +Require Compopts. Local Open Scope error_monad_scope. -Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f. +Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := Compopts.time name f. Definition transf_program (p: Mach.program) : res Asm.program := let mbp := (time "Machblock generation" Machblockgen.transf_program) p in |