From 0053b1aa1d26da5d1f995a603b127daf799c2da9 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 21 May 2012 16:26:30 +0000
Subject: Merge of the newmem branch: - Revised memory model with Max and Cur
 permissions, but without bounds - Constant propagation of 'const' globals -
 Function inlining at RTL level - (Unprovable) elimination of unreferenced
 static definitions

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1899 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 Makefile | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 2c2825c..8c73798 100644
--- a/Makefile
+++ b/Makefile
@@ -39,12 +39,13 @@ GPATH=$(DIRS)
 # General-purpose libraries (in lib/)
 
 LIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \
-  Iteration.v Integers.v Floats.v Parmov.v UnionFind.v
+  Iteration.v Integers.v Floats.v Parmov.v UnionFind.v Wfsimpl.v \
+  Postorder.v
 
 # Parts common to the front-ends and the back-end (in common/)
 
-COMMON=Errors.v AST.v Events.v Globalenvs.v Memdata.v Memtype.v Memory.v Values.v \
-  Smallstep.v Behaviors.v Switch.v Determinism.v
+COMMON=Errors.v AST.v Events.v Globalenvs.v Memdata.v Memtype.v Memory.v \
+  Values.v Smallstep.v Behaviors.v Switch.v Determinism.v
 
 # Back-end modules (in backend/, $(ARCH)/, $(ARCH)/$(VARIANT))
 
@@ -54,6 +55,8 @@ BACKEND=\
   Registers.v RTL.v \
   RTLgen.v RTLgenspec.v RTLgenproof.v \
   Tailcall.v Tailcallproof.v \
+  Inlining.v Inliningspec.v Inliningproof.v \
+  Renumber.v Renumberproof.v \
   RTLtyping.v \
   Kildall.v \
   ConstpropOp.v Constprop.v ConstpropOpproof.v Constpropproof.v \
-- 
cgit v1.2.3