1 files changed, 1 insertions, 2 deletions
diff --git a/kvx/Asm.v b/kvx/Asm.v
index 515e13e0..dc7ff6bd 100644
--- a/kvx/Asm.v
+++ b/kvx/Asm.v
@@ -35,13 +35,12 @@ 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.
-Definition preg := preg.
 
 Inductive addressing : Type :=
   | AOff (ofs: offset)