1 files changed, 0 insertions, 1 deletions
diff --git a/ia32/Op.v b/ia32/Op.v
index c32de67..8169594 100644
--- a/ia32/Op.v
+++ b/ia32/Op.v
@@ -29,7 +29,6 @@ Require Import AST.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
-Require Import Memdata.
 Require Import Memory.
 Require Import Globalenvs.
 Require Import Events.