From 3a2533890c9c275c38d620f4bcfa4aa76eab19a6 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 1 May 2013 09:57:08 +0000
Subject: Oops, removed a crucial declaration for Allocation.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2227 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 211569e..df155f1 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -19,6 +19,7 @@ Require RTLgen.
 Require Inlining.
 Require ConstpropOp.
 Require Constprop.
+Require Allocation.
 Require Compiler.
 
 (* Standard lib *)
@@ -72,6 +73,9 @@ Extract Constant ConstpropOp.propagate_float_constants =>
 Extract Constant Constprop.generate_float_constants =>
   "fun _ -> !Clflags.option_ffloatconstprop >= 2".
 
+(* Allocation *)
+Extract Constant Allocation.regalloc => "Regalloc.regalloc".
+
 (* Linearize *)
 Extract Constant Linearize.enumerate_aux => "Linearizeaux.enumerate_aux".
 
-- 
cgit v1.2.3