1 files changed, 3 insertions, 0 deletions
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)