diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-20 16:38:43 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-20 16:38:43 +0200 |
| commit | c5b3084dbb231fd8a97789799fd99d7012d59bed (patch) | |
| tree | aaef633ab25c6c1a5be5d4b5d170472912962c83 | |
| parent | 71cec9c9126ee4385ce12fd29dec557995d5a903 (diff) | |
| download | compcert-kvx-c5b3084dbb231fd8a97789799fd99d7012d59bed.tar.gz compcert-kvx-c5b3084dbb231fd8a97789799fd99d7012d59bed.zip | |
extraction problems
| -rw-r--r-- | extraction/extraction.v | 1 | ||||
| -rw-r--r-- | mppa_k1c/Asmgen.v | 3 |
2 files changed, 2 insertions, 2 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index ee45b756..e4c1cb25 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -136,7 +136,6 @@ Extract Constant Compiler.print_LTL => "PrintLTL.print_if". Extract Constant Compiler.print_Mach => "PrintMach.print_if". Extract Constant Compiler.print => "fun (f: 'a -> unit) (x: 'a) -> f x; x". Extract Constant Compiler.time => "Timing.time_coq". -Extract Constant Asmgen.time => "Timing.time_coq". (*Extraction Inline Compiler.apply_total Compiler.apply_partial.*) diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v index c3588871..e64e3df3 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -22,7 +22,8 @@ Require Import Errors String. 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 := + Compiler.time. Definition transf_program (p: Mach.program) : res Asm.program := let mbp := (time "Machblock generation" Machblockgen.transf_program) p in |