aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/extractionMachdep.v
diff options
context:
space:
mode:
Diffstat (limited to 'mppa_k1c/extractionMachdep.v')
-rw-r--r--mppa_k1c/extractionMachdep.v3
1 files changed, 3 insertions, 0 deletions
diff --git a/mppa_k1c/extractionMachdep.v b/mppa_k1c/extractionMachdep.v
index e70f51de..fdecd2a3 100644
--- a/mppa_k1c/extractionMachdep.v
+++ b/mppa_k1c/extractionMachdep.v
@@ -22,6 +22,9 @@ Require Archi Asm.
Extract Constant Archi.ptr64 => " Configuration.model = ""64"" ".
Extract Constant Archi.pic_code => "fun () -> false". (* for the time being *)
+Extract Constant Peephole.print_found_store =>
+"fun offset x -> Printf.printf ""found offset = %ld\n"" (Camlcoq.camlint_of_coqint offset); x".
+
(* Asm *)
(*
Extract Constant Asm.low_half => "fun _ _ _ -> assert false".