1 files changed, 5 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 7d5b222c..c126bfcb 100644
--- a/Makefile
+++ b/Makefile
@@ -122,9 +122,13 @@ BACKEND=\
   Debugvar.v Debugvarproof.v \
   Mach.v \
   Bounds.v Stacklayout.v Stacking.v Stackingproof.v \
-  Asm.v Asmgen.v Asmgenproof0.v Asmgenproof1.v Asmgenproof.v Asmaux.v \
+  Asm.v Asmgen.v Asmgenproof0.v Asmgenproof.v Asmaux.v \
   $(BACKENDLIB)
 
+ifneq ($(ARCH), "kvx")
+  BACKEND += Asmgenproof1.v 
+endif
+
 # C front-end modules (in cfrontend/)
 
 CFRONTEND=Ctypes.v Cop.v Csyntax.v Csem.v Ctyping.v Cstrategy.v Cexec.v \