6 files changed, 0 insertions, 17 deletions
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index b34d9395..8ef249dd 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -13,14 +13,10 @@
 (** Translation from Mach to PPC. *)
 
 Require Import Coqlib.
-Require Import Maps.
 Require Import Errors.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
-Require Import Values.
-Require Import Memory.
-Require Import Globalenvs.
 Require Import Op.
 Require Import Locations.
 Require Import Mach.
diff --git a/powerpc/Asmgenretaddr.v b/powerpc/Asmgenretaddr.v
index 081336ca..ddbfda65 100644
--- a/powerpc/Asmgenretaddr.v
+++ b/powerpc/Asmgenretaddr.v
@@ -17,13 +17,9 @@
     return addresses that are stored in activation records. *)
 
 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 Import Op.
 Require Import Locations.
 Require Import Mach.
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp
index c39ccdb1..973be925 100644
--- a/powerpc/ConstpropOp.vp
+++ b/powerpc/ConstpropOp.vp
@@ -17,7 +17,6 @@ Require Import Coqlib.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
-Require Import Values.
 Require Import Op.
 Require Import Registers.
 
diff --git a/powerpc/Op.v b/powerpc/Op.v
index 353c51c9..e59e15f1 100644
--- a/powerpc/Op.v
+++ b/powerpc/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.
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index fbd2d7b4..905a4489 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.
 
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 911327ce..5e493662 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -19,9 +19,7 @@ Require Import Integers.
 Require Import Floats.
 Require Import Values.
 Require Import Memory.
-Require Import Events.
 Require Import Globalenvs.
-Require Import Smallstep.
 Require Import Cminor.
 Require Import Op.
 Require Import CminorSel.