Merge branch 'kvx-work' into kvx-work-merge3.8

Conflicts:
	Makefile
	configure

1 files changed, 22 insertions, 3 deletions

diff --git a/Makefile b/Makefile
index f3e5aef5..8b2fb534 100644
--- a/Makefile
+++ b/Makefile
@@ -29,17 +29,23 @@ endif
 
 BACKENDLIB?=Asmgenproof0.v
 
-DIRS := lib common $(ARCHDIRS) backend cfrontend driver exportclight cparser
+DIRS := lib lib/Impure common $(ARCHDIRS) scheduling backend cfrontend driver \
+	exportclight cparser
+
+RECDIRS:=lib common $(ARCHDIRS) scheduling backend cfrontend driver flocq exportclight \
+  cparser
 
 COQINCLUDES := $(foreach d, $(DIRS), -R $(d) compcert.$(subst /,.,$d))
 
 ifeq ($(LIBRARY_FLOCQ),local)
 DIRS += flocq/Core flocq/Prop flocq/Calc flocq/IEEE754
+RECDIRS += flocq
 COQINCLUDES += -R flocq Flocq
 endif
 
 ifeq ($(LIBRARY_MENHIRLIB),local)
 DIRS += MenhirLib
+RECDIRS += MenhirLib
 COQINCLUDES += -R MenhirLib MenhirLib
 endif
 
@@ -75,7 +81,9 @@ VLIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \
   HashedSet.v \
   Iteration.v Zbits.v Integers.v Archi.v IEEE754_extra.v Floats.v \
   Parmov.v UnionFind.v Wfsimpl.v \
-  Postorder.v FSetAVLplus.v IntvSets.v Decidableplus.v BoolEqual.v
+  Postorder.v FSetAVLplus.v IntvSets.v Decidableplus.v BoolEqual.v \
+  ImpConfig.v  ImpExtern.v  ImpIO.v     ImpMonads.v \
+  ImpCore.v    ImpHCons.v   ImpLoops.v  ImpPrelude.v
 
 # Parts common to the front-ends and the back-end (in common/)
 
@@ -131,6 +139,13 @@ ifneq ($(ARCH),kvx)
   BACKEND += Asmgenproof1.v 
 endif
 
+SCHEDULING= \
+  RTLpathLivegenproof.v    RTLpathSE_simu_specs.v \
+  RTLpathLivegen.v         RTLpathSE_impl.v \
+  RTLpathproof.v           RTLpathSE_theory.v \
+  RTLpathSchedulerproof.v  RTLpath.v \
+  RTLpathScheduler.v
+
 # C front-end modules (in cfrontend/)
 
 CFRONTEND=Ctypes.v Cop.v Csyntax.v Csem.v Ctyping.v Cstrategy.v Cexec.v \
@@ -160,7 +175,7 @@ DRIVER=Compopts.v Compiler.v Complements.v
 
 # All source files
 
-FILES=$(VLIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER) $(FLOCQ) \
+FILES=$(VLIB) $(COMMON) $(BACKEND) $(SCHEDULING) $(CFRONTEND) $(DRIVER) $(FLOCQ) \
   $(MENHIRLIB) $(PARSER)
 
 # Generated source files
@@ -206,6 +221,10 @@ ccomp: .depend.extr compcert.ini driver/Version.ml FORCE
 ccomp.byte: .depend.extr compcert.ini driver/Version.ml FORCE
 	$(MAKE) -f Makefile.extr ccomp.byte
 
+# DM force compilation without checking dependencies
+ccomp.force: .depend.extr compcert.ini driver/Version.ml FORCE
+	$(MAKE) -f Makefile.extr ccomp.force
+
 clightgen: .depend.extr compcert.ini exportclight/Clightdefs.vo driver/Version.ml FORCE
 	$(MAKE) -f Makefile.extr clightgen
 clightgen.byte: .depend.extr compcert.ini exportclight/Clightdefs.vo driver/Version.ml FORCE