3 files changed, 7 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index 0327b729..f3e5aef5 100644
--- a/Makefile
+++ b/Makefile
@@ -27,6 +27,8 @@ else
 ARCHDIRS?=$(ARCH)_$(BITSIZE) $(ARCH)
 endif
 
+BACKENDLIB?=Asmgenproof0.v
+
 DIRS := lib common $(ARCHDIRS) backend cfrontend driver exportclight cparser
 
 COQINCLUDES := $(foreach d, $(DIRS), -R $(d) compcert.$(subst /,.,$d))
@@ -122,7 +124,7 @@ BACKEND=\
   Debugvar.v Debugvarproof.v \
   Mach.v \
   Bounds.v Stacklayout.v Stacking.v Stackingproof.v \
-  Asm.v Asmgen.v Asmgenproof0.v Asmgenproof.v Asmaux.v \
+  Asm.v Asmgen.v Asmgenproof.v Asmaux.v \
   $(BACKENDLIB)
 
 ifneq ($(ARCH),kvx)
diff --git a/Makefile.extr b/Makefile.extr
index 0f71c8e1..4f1c3c65 100644
--- a/Makefile.extr
+++ b/Makefile.extr
@@ -51,7 +51,7 @@ INCLUDES=$(patsubst %,-I %, $(DIRS))
 # Control of warnings:
 
 # WARNINGS=-w +a-4-9-27-42 -strict-sequence -safe-string -warn-error +a #Deprication returns with ocaml 4.03
-WARNINGS=-w +a-4-9-27
+WARNINGS=-w +a-4-9-27-42
 
 extraction/%.cmx: WARNINGS +=-w -20-27-32..34-39-41-44..45-60-67
 extraction/%.cmo: WARNINGS +=-w -20-27-32..34-39-41-44..45-60-67
diff --git a/kvx/Asm.v b/kvx/Asm.v
index dc7ff6bd..6d8736af 100644
--- a/kvx/Asm.v
+++ b/kvx/Asm.v
@@ -42,6 +42,9 @@ Require Import Errors.
 (** Definitions for OCaml code *)
 Definition label := positive.
 
+(* Necessary definition for Asmexpandaux.mli *)
+Definition preg := preg.
+
 Inductive addressing : Type :=
   | AOff (ofs: offset)
   | AReg (ro: ireg)