From f2fb8540c94ceb9892510f83bd7d6734fe9d422f Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Fri, 4 Dec 2020 17:19:46 +0100
Subject: Fixing compilation for KVX

---
 Makefile      | 4 +++-
 Makefile.extr | 2 +-
 kvx/Asm.v     | 3 +++
 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)
-- 
cgit