From 255cee09b71255051c2b40eae0c88bffce1f6f32 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sat, 20 Apr 2013 07:54:52 +0000
Subject: Big merge of the newregalloc-int64 branch.  Lots of changes in two
 directions: 1- new register allocator (+ live range splitting,
 spilling&reloading, etc)    based on a posteriori validation using the
 Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long
 long").

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 Makefile | 19 ++++++++-----------
 1 file changed, 8 insertions(+), 11 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index fed2660b..0db41182 100644
--- a/Makefile
+++ b/Makefile
@@ -55,7 +55,7 @@ FLOCQ=$(FLOCQ_CORE) $(FLOCQ_PROP) $(FLOCQ_CALC) $(FLOCQ_APPLI)
 
 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 Wfsimpl.v \
-  Postorder.v
+  Postorder.v FSetAVLplus.v
 
 # Parts common to the front-ends and the back-end (in common/)
 
@@ -66,7 +66,8 @@ COMMON=Errors.v AST.v Events.v Globalenvs.v Memdata.v Memtype.v Memory.v \
 
 BACKEND=\
   Cminor.v Op.v CminorSel.v \
-  SelectOp.v Selection.v SelectOpproof.v Selectionproof.v \
+  SelectOp.v SelectLong.v Selection.v \
+  SelectOpproof.v SelectLongproof.v Selectionproof.v \
   Registers.v RTL.v \
   RTLgen.v RTLgenspec.v RTLgenproof.v \
   Tailcall.v Tailcallproof.v \
@@ -76,16 +77,12 @@ BACKEND=\
   Kildall.v Liveness.v \
   ConstpropOp.v Constprop.v ConstpropOpproof.v Constpropproof.v \
   CombineOp.v CSE.v CombineOpproof.v CSEproof.v \
-  Machregs.v Locations.v Conventions1.v Conventions.v LTL.v LTLtyping.v \
-  InterfGraph.v Coloring.v Coloringproof.v \
-  Allocation.v Allocproof.v Alloctyping.v \
-  Tunneling.v Tunnelingproof.v Tunnelingtyping.v \
-  LTLin.v LTLintyping.v \
-  Linearize.v Linearizeproof.v Linearizetyping.v \
-  CleanupLabels.v CleanupLabelsproof.v CleanupLabelstyping.v \
+  Machregs.v Locations.v Conventions1.v Conventions.v LTL.v \
+  Allocation.v Allocproof.v \
+  Tunneling.v Tunnelingproof.v \
   Linear.v Lineartyping.v \
-  Parallelmove.v Reload.v Reloadproof.v Reloadtyping.v \
-  RRE.v RREproof.v RREtyping.v \
+  Linearize.v Linearizeproof.v \
+  CleanupLabels.v CleanupLabelsproof.v \
   Mach.v \
   Bounds.v Stacklayout.v Stacking.v Stackingproof.v \
   Asm.v Asmgen.v Asmgenproof0.v Asmgenproof1.v Asmgenproof.v
-- 
cgit