Remove some useless "Require".

Update ARM port.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2085 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

10 files changed, 0 insertions, 23 deletions

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.