From a74f6b45d72834b5b8417297017bd81424123d98 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 7 Mar 2010 15:52:58 +0000 Subject: Merge of the newmem and newextcalls branches: - Revised memory model with concrete representation of ints & floats, and per-byte access permissions - Revised Globalenvs implementation - Matching changes in all languages and proofs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1282 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index c9a61d72..d50a4788 100644 --- a/Makefile +++ b/Makefile @@ -33,12 +33,12 @@ GPATH=$(DIRS) # General-purpose libraries (in lib/) -LIB=Coqlib.v Maps.v Lattice.v Ordered.v \ +LIB=Coqlib.v Intv.v Maps.v Lattice.v Ordered.v \ Iteration.v Integers.v Floats.v Parmov.v UnionFind.v # Parts common to the front-ends and the back-end (in common/) -COMMON=Errors.v AST.v Events.v Globalenvs.v Mem.v Values.v \ +COMMON=Errors.v AST.v Events.v Globalenvs.v Memdata.v Memtype.v Memory.v Values.v \ Smallstep.v Determinism.v Switch.v # Back-end modules (in backend/, $(ARCH)/, $(ARCH)/$(VARIANT)) -- cgit