aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile7
1 files changed, 1 insertions, 6 deletions
diff --git a/Makefile b/Makefile
index c9255fdb..10c4f4bf 100644
--- a/Makefile
+++ b/Makefile
@@ -152,15 +152,10 @@ 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 \
+ 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