From 5bf13140754a55599ae27942b17cdbb4b7ed74e9 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 30 Dec 2012 17:47:53 +0000
Subject: Remove some useless "Require". Update ARM port.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2085 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 powerpc/Asmgen.v        | 4 ----
 powerpc/Asmgenretaddr.v | 4 ----
 powerpc/ConstpropOp.vp  | 1 -
 powerpc/Op.v            | 1 -
 powerpc/SelectOp.vp     | 5 -----
 powerpc/SelectOpproof.v | 2 --
 6 files changed, 17 deletions(-)

(limited to 'powerpc')

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.
-- 
cgit