diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-04 15:33:05 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-04 15:33:05 +0000 |
commit | a7c6cf8d4d59e29ed73f9eb8bfc015b0384672a1 (patch) | |
tree | 3abfe8b71f399e1f73cd33fd618100f5a421351c /Makefile | |
parent | 73729d23ac13275c0d28d23bc1b1f6056104e5d9 (diff) |
Revu la repartition des sources Coq en sous-repertoires
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@73 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'Makefile')
-rw-r--r-- | Makefile | 17 |
1 files changed, 10 insertions, 7 deletions
@@ -2,19 +2,22 @@ COQC=coqc $(INCLUDES) COQDEP=coqdep $(INCLUDES) COQDOC=coqdoc -INCLUDES=-I lib -I backend -I cfrontend +INCLUDES=-I lib -I common -I backend -I cfrontend # Files in lib/ LIB=Coqlib.v Maps.v Sets.v union_find.v Inclusion.v Lattice.v Ordered.v \ Iteration.v Integers.v Floats.v Parmov.v +# Files in common/ + +COMMON=AST.v Events.v Globalenvs.v Mem.v Values.v Main.v + # Files in backend/ -BACKEND=AST.v Values.v Mem.v Events.v Globalenvs.v \ +BACKEND=\ Op.v Cminor.v \ Cmconstr.v Cmconstrproof.v \ - Csharpminor.v Cminorgen.v Cminorgenproof.v \ Registers.v RTL.v \ RTLgen.v RTLgenproof1.v RTLgenproof.v \ RTLtyping.v \ @@ -31,17 +34,17 @@ BACKEND=AST.v Values.v Mem.v Events.v Globalenvs.v \ Mach.v Machabstr.v Machtyping.v \ Stacking.v Stackingproof.v Stackingtyping.v \ Machabstr2mach.v \ - PPC.v PPCgen.v PPCgenproof1.v PPCgenproof.v \ - Main.v + PPC.v PPCgen.v PPCgenproof1.v PPCgenproof.v # Files in cfrontend/ CFRONTEND=Csyntax.v Csem.v Ctyping.v Cshmgen.v \ - Cshmgenproof1.v Cshmgenproof2.v Cshmgenproof3.v + Cshmgenproof1.v Cshmgenproof2.v Cshmgenproof3.v \ + Csharpminor.v Cminorgen.v Cminorgenproof.v # All source files -FILES=$(LIB:%=lib/%) $(BACKEND:%=backend/%) $(CFRONTEND:%=cfrontend/%) +FILES=$(LIB:%=lib/%) $(COMMON:%=common/%) $(BACKEND:%=backend/%) $(CFRONTEND:%=cfrontend/%) FLATFILES=$(LIB) $(BACKEND) $(CFRONTEND) |