From 73729d23ac13275c0d28d23bc1b1f6056104e5d9 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 4 Sep 2006 15:08:29 +0000
Subject: Fusion de la branche "traces": - Ajout de traces d'evenements d'E/S
 dans les semantiques - Ajout constructions switch et allocation dynamique -
 Initialisation des variables globales - Portage Coq 8.1 beta Debut
 d'integration du front-end C: - Traduction Clight -> Csharpminor dans
 cfrontend/ - Modifications de Csharpminor et Globalenvs en consequence.

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

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 6900b3db..8df29edc 100644
--- a/Makefile
+++ b/Makefile
@@ -2,16 +2,16 @@ COQC=coqc $(INCLUDES)
 COQDEP=coqdep $(INCLUDES)
 COQDOC=coqdoc
 
-INCLUDES=-I lib -I backend
+INCLUDES=-I lib -I backend -I cfrontend
 
 # Files in lib/
 
 LIB=Coqlib.v Maps.v Sets.v union_find.v Inclusion.v Lattice.v Ordered.v \
-  Integers.v Floats.v
+  Iteration.v Integers.v Floats.v Parmov.v
 
 # Files in backend/
 
-BACKEND=AST.v Values.v Mem.v Globalenvs.v \
+BACKEND=AST.v Values.v Mem.v Events.v Globalenvs.v \
   Op.v Cminor.v \
   Cmconstr.v Cmconstrproof.v \
   Csharpminor.v Cminorgen.v Cminorgenproof.v \
@@ -24,8 +24,7 @@ BACKEND=AST.v Values.v Mem.v Globalenvs.v \
   Locations.v Conventions.v LTL.v LTLtyping.v \
   InterfGraph.v Coloring.v Coloringproof.v \
   Parallelmove.v Allocation.v \
-  Allocproof_aux.v Allocproof.v \
-  Alloctyping_aux.v Alloctyping.v \
+  Allocproof.v Alloctyping.v \
   Tunneling.v Tunnelingproof.v Tunnelingtyping.v \
   Linear.v Lineartyping.v \
   Linearize.v Linearizeproof.v Linearizetyping.v \
@@ -35,11 +34,16 @@ BACKEND=AST.v Values.v Mem.v Globalenvs.v \
   PPC.v PPCgen.v PPCgenproof1.v PPCgenproof.v \
   Main.v
 
+# Files in cfrontend/
+
+CFRONTEND=Csyntax.v Csem.v Ctyping.v Cshmgen.v \
+  Cshmgenproof1.v Cshmgenproof2.v Cshmgenproof3.v 
+
 # All source files
 
-FILES=$(LIB:%=lib/%) $(BACKEND:%=backend/%)
+FILES=$(LIB:%=lib/%) $(BACKEND:%=backend/%) $(CFRONTEND:%=cfrontend/%)
 
-FLATFILES=$(LIB) $(BACKEND)
+FLATFILES=$(LIB) $(BACKEND) $(CFRONTEND)
 
 proof: $(FILES:.v=.vo)
 
-- 
cgit