1 files changed, 0 insertions, 5 deletions
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index fbd2d7b..905a448 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/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.