From a3319eb05543930844dedd9ac31ed1beaac3047e Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 20 Jul 2021 15:21:29 +0200 Subject: Fix compile on ARM/x86 backends --- Makefile | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) (limited to 'Makefile') 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 -- cgit