From 0be44be49c5be412a9d23e37c7b4554a9049ecbe Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 17 Nov 2013 16:18:46 +0000
Subject: Revised modeling of external functions and built-in functions: just
 axiomatize them.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2369 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 extraction/extraction.v | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'extraction')

diff --git a/extraction/extraction.v b/extraction/extraction.v
index 047a9b4..34e6b0a 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -23,6 +23,7 @@ Require Constprop.
 Require Tailcall.
 Require Allocation.
 Require Compiler.
+Require Cexec.
 
 (* Standard lib *)
 Require Import ExtrOcamlBasic.
@@ -106,6 +107,9 @@ Extract Constant Compiler.print_Mach => "PrintMach.print_if".
 Extract Constant Compiler.print => "fun (f: 'a -> unit) (x: 'a) -> f x; x".
 (*Extraction Inline Compiler.apply_total Compiler.apply_partial.*)
 
+(* Reference interpreter *)
+Extract Constant Cexec.do_external_function => "Interp_ext.do_external_function".
+
 (* Processor-specific extraction directives *)
 
 Load extractionMachdep.
-- 
cgit v1.2.3