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
---
 ia32/Asmgen.v           | 4 ----
 ia32/Asmgenproof.v      | 1 -
 ia32/Asmgenproof1.v     | 1 -
 ia32/Asmgenretaddr.v    | 4 ----
 ia32/CombineOpproof.v   | 2 --
 ia32/ConstpropOp.vp     | 1 -
 ia32/ConstpropOpproof.v | 1 -
 ia32/Op.v               | 1 -
 ia32/SelectOp.vp        | 5 -----
 ia32/SelectOpproof.v    | 3 ---
 10 files changed, 23 deletions(-)

(limited to 'ia32')

diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v
index 5a6c1ab..6b7cbf9 100644
--- a/ia32/Asmgen.v
+++ b/ia32/Asmgen.v
@@ -13,14 +13,10 @@
 (** Translation from Mach to IA32 Asm. *)
 
 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/ia32/Asmgenproof.v b/ia32/Asmgenproof.v
index a49a7ff..3d0c57f 100644
--- a/ia32/Asmgenproof.v
+++ b/ia32/Asmgenproof.v
@@ -13,7 +13,6 @@
 (** Correctness proof for x86 generation: main proof. *)
 
 Require Import Coqlib.
-Require Import Maps.
 Require Import Errors.
 Require Import AST.
 Require Import Integers.
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v
index 7ad8a02..0a46677 100644
--- a/ia32/Asmgenproof1.v
+++ b/ia32/Asmgenproof1.v
@@ -13,7 +13,6 @@
 (** Correctness proof for IA32 generation: auxiliary results. *)
 
 Require Import Coqlib.
-Require Import Maps.
 Require Import AST.
 Require Import Errors.
 Require Import Integers.
diff --git a/ia32/Asmgenretaddr.v b/ia32/Asmgenretaddr.v
index 1a1ea20..29d2ba0 100644
--- a/ia32/Asmgenretaddr.v
+++ b/ia32/Asmgenretaddr.v
@@ -17,14 +17,10 @@
     return addresses that are stored in activation records. *)
 
 Require Import Coqlib.
-Require Import Maps.
 Require Import AST.
 Require Import Errors.
 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/ia32/CombineOpproof.v b/ia32/CombineOpproof.v
index cd10698..d4565bd 100644
--- a/ia32/CombineOpproof.v
+++ b/ia32/CombineOpproof.v
@@ -14,12 +14,10 @@
   during the [CSE] phase. *)
 
 Require Import Coqlib.
-Require Import AST.
 Require Import Integers.
 Require Import Values.
 Require Import Memory.
 Require Import Op.
-Require Import Registers.
 Require Import RTL.
 Require Import CombineOp.
 Require Import CSE.
diff --git a/ia32/ConstpropOp.vp b/ia32/ConstpropOp.vp
index ff5044f..8a612f0 100644
--- a/ia32/ConstpropOp.vp
+++ b/ia32/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/ia32/ConstpropOpproof.v b/ia32/ConstpropOpproof.v
index ca38f6b..1a0508c 100644
--- a/ia32/ConstpropOpproof.v
+++ b/ia32/ConstpropOpproof.v
@@ -13,7 +13,6 @@
 (** Correctness proof for constant propagation (processor-dependent part). *)
 
 Require Import Coqlib.
-Require Import AST.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
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.
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.
 
diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v
index f88f9c0..136a765 100644
--- a/ia32/SelectOpproof.v
+++ b/ia32/SelectOpproof.v
@@ -13,15 +13,12 @@
 (** Correctness of instruction selection for operators *)
 
 Require Import Coqlib.
-Require Import Maps.
 Require Import AST.
 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 v1.2.3