1 files changed, 6 insertions, 1 deletions
diff --git a/kvx/Asm.v b/kvx/Asm.v
index 515e13e0..fd20316c 100644
--- a/kvx/Asm.v
+++ b/kvx/Asm.v
@@ -35,12 +35,14 @@ Require Import Smallstep.
 Require Import Locations.
 Require Stacklayout.
 Require Import Conventions.
-Require Import Asmvliw.
+Require Export Asmvliw.
 Require Import Linking.
 Require Import Errors.
 
 (** Definitions for OCaml code *)
 Definition label := positive.
+
+(* Necessary definition for Asmexpandaux.mli *)
 Definition preg := preg.
 
 Inductive addressing : Type :=
@@ -102,6 +104,9 @@ Inductive instruction : Type :=
   | Palclrd (dst: ireg) (addr: ireg)
   | Palclrw (dst: ireg) (addr: ireg)
   | Pclzll (rd rs: ireg)
+  | Pclzw  (rd rs: ireg)
+  | Pctzll (rd rs: ireg)
+  | Pctzw  (rd rs: ireg)
   | Pstsud (rd rs1 rs2: ireg)
             
   (** Loads *)