From d18371174552ed29069a34d81d60530df431ac0f Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 1 May 2013 12:37:36 +0000
Subject: Use "-as" to put CompCert modules in a compcert.xxx namespace.
 Simplified the scripts "coq" and "pg". Updated deps.

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

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 0db4118..cced7da 100644
--- a/Makefile
+++ b/Makefile
@@ -13,22 +13,28 @@
 include Makefile.config
 
 DIRS=lib common $(ARCH)/$(VARIANT) $(ARCH) backend cfrontend driver \
-  flocq/Core flocq/Prop flocq/Calc flocq/Appli
+  flocq/Core flocq/Prop flocq/Calc flocq/Appli exportclight
 
-INCLUDES=$(patsubst %,-I %, $(DIRS))
+RECDIRS=lib common backend cfrontend driver flocq exportclight
 
-COQC=coqc -q $(INCLUDES)
-COQDEP=coqdep $(INCLUDES)
+COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) -as compcert.$(d)) \
+  -I $(ARCH)/$(VARIANT) -as compcert.$(ARCH).$(VARIANT) \
+  -I $(ARCH) -as compcert.$(ARCH)
+
+CAMLINCLUDES=$(patsubst %,-I %, $(DIRS)) -I extraction -I cparser
+
+COQC=coqc -q $(COQINCLUDES)
+COQDEP=coqdep $(COQINCLUDES)
 COQDOC=coqdoc
-COQEXEC=coqtop $(INCLUDES) -batch -load-vernac-source
-COQCHK=coqchk $(INCLUDES)
+COQEXEC=coqtop $(COQINCLUDES) -batch -load-vernac-source
+COQCHK=coqchk $(COQINCLUDES)
 
 OCAMLBUILD=ocamlbuild
 OCB_OPTIONS=\
   -j 2 \
   -no-hygiene \
   -no-links \
-  -I extraction -I cparser $(INCLUDES)
+  $(CAMLINCLUDES)
 OCB_OPTIONS_CHECKLINK=\
   $(OCB_OPTIONS) \
   -I checklink \
@@ -251,6 +257,9 @@ check-admitted: $(FILES)
 check-proof: $(FILES)
 	$(COQCHK) -admit Integers -admit Floats -admit AST -admit Asm -admit Mach -admit UnionFind Complements 
 
+print-includes:
+	@echo $(COQINCLUDES)
+
 include .depend
 
 FORCE:
-- 
cgit v1.2.3