[MERGE] BTL into kvx-work (replacing RTLpath)

1 files changed, 5 insertions, 6 deletions

diff --git a/Makefile b/Makefile
index 05e4cbcd..3039a375 100644
--- a/Makefile
+++ b/Makefile
@@ -100,6 +100,7 @@ VLIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.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 \
+  OptionMonad.v \
   ImpConfig.v  ImpExtern.v  ImpIO.v     ImpMonads.v \
   ImpCore.v    ImpHCons.v   ImpLoops.v  ImpPrelude.v
 
@@ -152,15 +153,13 @@ BACKEND=\
   Mach.v \
   Bounds.v Stacklayout.v Stacking.v Stackingproof.v \
   Asm.v Asmgen.v Asmgenproof.v Asmaux.v \
-	RTLpathSE_simplify.v \
+	BTL_SEsimplify.v \
   $(BACKENDLIB)
 
 SCHEDULING= \
-  RTLpathLivegenproof.v    RTLpathSE_simu_specs.v \
-  RTLpathLivegen.v         RTLpathSE_impl.v \
-  RTLpathproof.v           RTLpathSE_theory.v \
-  RTLpathSchedulerproof.v  RTLpath.v \
-  RTLpathScheduler.v       RTLpathWFcheck.v
+  BTL.v BTLmatchRTL.v BTLtoRTL.v BTLtoRTLproof.v RTLtoBTL.v RTLtoBTLproof.v \
+  BTL_Livecheck.v BTL_Scheduler.v BTL_Schedulerproof.v\
+	BTL_SEtheory.v BTL_SEsimuref.v BTL_SEimpl.v
 
 # C front-end modules (in cfrontend/)