From 355b4abcee015c3fae9ac5653c25259e104a886c Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sat, 4 Aug 2007 07:27:50 +0000
Subject: Fusion des modifications faites sur les branches "tailcalls" et
 "smallstep". En particulier: - Semantiques small-step depuis RTL jusqu'a PPC
 - Cminor independant du processeur - Ajout passes Selection et Reload - Ajout
 des langages intermediaires CminorSel et LTLin correspondants - Ajout des
 tailcalls depuis Cminor jusqu'a PPC

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

(limited to 'extraction/extraction.v')

diff --git a/extraction/extraction.v b/extraction/extraction.v
index 47c6f36c..cc33c981 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -38,6 +38,7 @@ Extract Constant Iteration.GenIter.iterate =>
 
 
 (* RTLgen *)
+Extract Constant RTLgen.compile_switch => "RTLgenaux.compile_switch".
 Extract Constant RTLgen.more_likely => "RTLgenaux.more_likely".
 
 (* RTLtyping *)
-- 
cgit