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

---
 kvx/Asm.v | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kvx/Asm.v')

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