diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-20 17:07:16 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-20 17:07:16 +0200 |
| commit | adc142066720798ca2e6f7709de6fba93559a336 (patch) | |
| tree | 2ac7f45e40dc26354a6c7c9896d0b80b87b61422 /mppa_k1c/Asmgen.v | |
| parent | c5b3084dbb231fd8a97789799fd99d7012d59bed (diff) | |
| download | compcert-kvx-adc142066720798ca2e6f7709de6fba93559a336.tar.gz compcert-kvx-adc142066720798ca2e6f7709de6fba93559a336.zip | |
fix compiling
Diffstat (limited to 'mppa_k1c/Asmgen.v')
| -rw-r--r-- | mppa_k1c/Asmgen.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v index e64e3df3..8875a4ac 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -19,11 +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 := - Compiler.time. +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 |