1 files changed, 0 insertions, 5 deletions
diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp
index 7bb2bee..0c30386 100644
--- a/ia32/SelectOp.vp
+++ b/ia32/SelectOp.vp
@@ -37,14 +37,9 @@
 *)
 
 Require Import Coqlib.
-Require Import Maps.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
-Require Import Values.
-Require Import Memory.
-Require Import Globalenvs.
-Require Cminor.
 Require Import Op.
 Require Import CminorSel.