Remove some useless "Require".

Update ARM port.


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

45 files changed, 6 insertions, 90 deletions

diff --git a/backend/Allocation.v b/backend/Allocation.v
index 508bc13..4a4c219 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -17,16 +17,12 @@ Require Import Errors.
 Require Import Maps.
 Require Import Lattice.
 Require Import AST.
-Require Import Integers.
-Require Import Values.
-Require Import Globalenvs.
 Require Import Op.
 Require Import Registers.
 Require Import RTL.
 Require Import RTLtyping.
 Require Import Kildall.
 Require Import Locations.
-Require Import Conventions.
 Require Import Coloring.
 
 (** * Liveness analysis over RTL *)
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index a9477e0..2011485 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -14,7 +14,6 @@
   RTL to LTL). *)
 
 Require Import FSets.
-Require Import SetoidList.
 Require Import Coqlib.
 Require Import Errors.
 Require Import Maps.
diff --git a/backend/Bounds.v b/backend/Bounds.v
index 23fa3b5..ef78b2e 100644
--- a/backend/Bounds.v
+++ b/backend/Bounds.v
@@ -13,7 +13,6 @@
 (** Computation of resource bounds for Linear code. *)
 
 Require Import Coqlib.
-Require Import Maps.
 Require Import AST.
 Require Import Op.
 Require Import Locations.
diff --git a/backend/CSE.v b/backend/CSE.v
index 85f46e2..1888fb8 100644
--- a/backend/CSE.v
+++ b/backend/CSE.v
@@ -21,7 +21,6 @@ Require Import Integers.
 Require Import Floats.
 Require Import Values.
 Require Import Memory.
-Require Import Globalenvs.
 Require Import Op.
 Require Import Registers.
 Require Import RTL.
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index 49b213b..5569123 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -16,8 +16,6 @@ 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 Events.
diff --git a/backend/CleanupLabels.v b/backend/CleanupLabels.v
index 7401abc..0ed2be1 100644
--- a/backend/CleanupLabels.v
+++ b/backend/CleanupLabels.v
@@ -21,7 +21,6 @@
   branched to. *)
 
 Require Import Coqlib.
-Require Import Maps.
 Require Import Ordered.
 Require Import FSets.
 Require FSetAVL.
diff --git a/backend/CleanupLabelsproof.v b/backend/CleanupLabelsproof.v
index a7a60f6..dbd33c1 100644
--- a/backend/CleanupLabelsproof.v
+++ b/backend/CleanupLabelsproof.v
@@ -13,7 +13,6 @@
 (** Correctness proof for clean-up of labels *)
 
 Require Import Coqlib.
-Require Import Maps.
 Require Import Ordered.
 Require Import FSets.
 Require Import AST.
@@ -22,7 +21,6 @@ Require Import Values.
 Require Import Memory.
 Require Import Events.
 Require Import Globalenvs.
-Require Import Errors.
 Require Import Smallstep.
 Require Import Op.
 Require Import Locations.
diff --git a/backend/CleanupLabelstyping.v b/backend/CleanupLabelstyping.v
index ea9de86..f58a910 100644
--- a/backend/CleanupLabelstyping.v
+++ b/backend/CleanupLabelstyping.v
@@ -14,7 +14,6 @@
 
 Require Import Coqlib.
 Require Import Maps.
-Require Import Errors.
 Require Import AST.
 Require Import Op.
 Require Import Locations.
diff --git a/backend/CminorSel.v b/backend/CminorSel.v
index a063544..b5a0d39 100644
--- a/backend/CminorSel.v
+++ b/backend/CminorSel.v
@@ -16,7 +16,6 @@ Require Import Coqlib.
 Require Import Maps.
 Require Import AST.
 Require Import Integers.
-Require Import Floats.
 Require Import Events.
 Require Import Values.
 Require Import Memory.
diff --git a/backend/Constprop.v b/backend/Constprop.v
index fc242e1..fe16240 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -19,8 +19,6 @@ Require Import Maps.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
-Require Import Values.
-Require Import Globalenvs.
 Require Import Op.
 Require Import Registers.
 Require Import RTL.
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index f14e87a..1b90666 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -16,7 +16,6 @@ Require Import Coqlib.
 Require Import Maps.
 Require Import AST.
 Require Import Integers.
-Require Import Floats.
 Require Import Values.
 Require Import Events.
 Require Import Memory.
diff --git a/backend/Inlining.v b/backend/Inlining.v
index 3ddfe9a..5075fd6 100644
--- a/backend/Inlining.v
+++ b/backend/Inlining.v
@@ -18,7 +18,6 @@ Require Import Errors.
 Require Import Maps.
 Require Import AST.
 Require Import Integers.
-Require Import Values.
 Require Import Op.
 Require Import Registers.
 Require Import RTL.
diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v
index 84bcdcd..014986d 100644
--- a/backend/Inliningspec.v
+++ b/backend/Inliningspec.v
@@ -18,7 +18,6 @@ Require Import Errors.
 Require Import Maps.
 Require Import AST.
 Require Import Integers.
-Require Import Values.
 Require Import Globalenvs.
 Require Import Op.
 Require Import Registers.
diff --git a/backend/InterfGraph.v b/backend/InterfGraph.v
index ec64e99..9a5522d 100644
--- a/backend/InterfGraph.v
+++ b/backend/InterfGraph.v
@@ -15,7 +15,6 @@
 Require Import Coqlib.
 Require Import FSets.
 Require Import FSetAVL.
-Require Import Maps.
 Require Import Ordered.
 Require Import Registers.
 Require Import Locations.
diff --git a/backend/LTLin.v b/backend/LTLin.v
index 390c4cf..e0d5ca2 100644
--- a/backend/LTLin.v
+++ b/backend/LTLin.v
@@ -17,7 +17,6 @@
     instructions with explicit labels and ``goto'' instructions. *)
 
 Require Import Coqlib.
-Require Import Maps.
 Require Import AST.
 Require Import Integers.
 Require Import Values.
@@ -28,7 +27,6 @@ Require Import Smallstep.
 Require Import Op.
 Require Import Locations.
 Require Import LTL.
-Require Import Conventions.
 
 (** * Abstract syntax *)
 
diff --git a/backend/LTLintyping.v b/backend/LTLintyping.v
index e9cc2df..0338667 100644
--- a/backend/LTLintyping.v
+++ b/backend/LTLintyping.v
@@ -13,12 +13,9 @@
 (** Typing rules for LTLin. *)
 
 Require Import Coqlib.
-Require Import Maps.
 Require Import AST.
 Require Import Integers.
-Require Import Memdata.
 Require Import Op.
-Require Import RTL.
 Require Import Locations.
 Require Import LTLin.
 Require LTLtyping.
diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v
index 2e627e9..0c90514 100644
--- a/backend/LTLtyping.v
+++ b/backend/LTLtyping.v
@@ -16,9 +16,7 @@ Require Import Coqlib.
 Require Import Maps.
 Require Import AST.
 Require Import Integers.
-Require Import Memdata.
 Require Import Op.
-Require Import RTL.
 Require Import Locations.
 Require Import LTL.
 Require Import Conventions.
diff --git a/backend/Linear.v b/backend/Linear.v
index b218531..52f5fd7 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -18,7 +18,6 @@
     [Lsetstack] are provided to access stack slots. *)
 
 Require Import Coqlib.
-Require Import Maps.
 Require Import AST.
 Require Import Integers.
 Require Import Values.
diff --git a/backend/Linearize.v b/backend/Linearize.v
index fd350c7..636cb22 100644
--- a/backend/Linearize.v
+++ b/backend/Linearize.v
@@ -19,8 +19,6 @@ Require Import Ordered.
 Require Import FSets.
 Require FSetAVL.
 Require Import AST.
-Require Import Values.
-Require Import Globalenvs.
 Require Import Errors.
 Require Import Op.
 Require Import Locations.
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index da73b00..32d6045 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -13,7 +13,6 @@
 (** Typing rules for Linear. *)
 
 Require Import Coqlib.
-Require Import Maps.
 Require Import AST.
 Require Import Integers.
 Require Import Values.
diff --git a/backend/Locations.v b/backend/Locations.v
index 0b538fd..ba2fb06 100644
--- a/backend/Locations.v
+++ b/backend/Locations.v
@@ -14,7 +14,6 @@
   the results of register allocation (file [Allocation]). *)
 
 Require Import Coqlib.
-Require Import Maps.
 Require Import AST.
 Require Import Values.
 Require Export Machregs.
diff --git a/backend/Mach.v b/backend/Mach.v
index 669d35e..56c0369 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -21,10 +21,7 @@ Require Import Maps.
 Require Import AST.
 Require Import Integers.
 Require Import Values.
-Require Import Memory.
-Require Import Events.
 Require Import Globalenvs.
-Require Import Smallstep.
 Require Import Op.
 Require Import Locations.
 Require Import Conventions.
diff --git a/backend/Machsem.v b/backend/Machsem.v
index a802323..6d5f1cf 100644
--- a/backend/Machsem.v
+++ b/backend/Machsem.v
@@ -13,7 +13,6 @@
 (** The Mach intermediate language: operational semantics. *)
 
 Require Import Coqlib.
-Require Import Maps.
 Require Import AST.
 Require Import Integers.
 Require Import Values.
diff --git a/backend/Machtyping.v b/backend/Machtyping.v
index b9d8009..2dc19be 100644
--- a/backend/Machtyping.v
+++ b/backend/Machtyping.v
@@ -13,14 +13,8 @@
 (** Type system for the Mach intermediate language. *)
 
 Require Import Coqlib.
-Require Import Maps.
 Require Import AST.
-Require Import Memory.
 Require Import Integers.
-Require Import Values.
-Require Import Memory.
-Require Import Events.
-Require Import Globalenvs.
 Require Import Op.
 Require Import Locations.
 Require Import Conventions.
diff --git a/backend/Parallelmove.v b/backend/Parallelmove.v
index d7a4217..4930ccd 100644
--- a/backend/Parallelmove.v
+++ b/backend/Parallelmove.v
@@ -24,7 +24,6 @@
 Require Import Coqlib.
 Require Parmov.
 Require Import Values.
-Require Import Events.
 Require Import AST.
 Require Import Locations.
 Require Import Conventions.
diff --git a/backend/RRE.v b/backend/RRE.v
index 95eadce..ece6051 100644
--- a/backend/RRE.v
+++ b/backend/RRE.v
@@ -13,10 +13,7 @@
 (** Redundant Reloads Elimination *)
 
 Require Import Coqlib.
-Require Import Maps.
 Require Import AST.
-Require Import Values.
-Require Import Globalenvs.
 Require Import Op.
 Require Import Locations.
 Require Import Conventions.
diff --git a/backend/RREproof.v b/backend/RREproof.v
index d70a1fd..8926fe4 100644
--- a/backend/RREproof.v
+++ b/backend/RREproof.v
@@ -14,7 +14,6 @@
 
 Require Import Axioms.
 Require Import Coqlib.
-Require Import Maps.
 Require Import AST.
 Require Import Values.
 Require Import Globalenvs.
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index 62df254..007191a 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -17,7 +17,6 @@ Require Errors.
 Require Import Maps.
 Require Import AST.
 Require Import Integers.
-Require Import Values.
 Require Import Switch.
 Require Import Op.
 Require Import Registers.
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index 1b8e853..690611c 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -617,9 +617,10 @@ Proof.
   edestruct Mem.loadv_extends as [v' []]; eauto.
   exists (rs1#rd <- v').
 (* Exec *)
-  split. eapply star_right. eexact EX1. eapply exec_Iload; eauto.
-  rewrite (@eval_addressing_preserved _ _ _ _ ge tge). eauto.
-  exact symbols_preserved. traceEq.
+  split. eapply star_right. eexact EX1. eapply exec_Iload. eauto.
+  instantiate (1 := vaddr'). rewrite <- H3.
+  apply eval_addressing_preserved. exact symbols_preserved.
+  auto. traceEq.
 (* Match-env *)
   split. eauto with rtlg. 
 (* Result *)
@@ -1049,9 +1050,9 @@ Proof.
   edestruct Mem.storev_extends as [tm' []]; eauto.
   econstructor; split.
   left; eapply plus_right. eapply star_trans. eexact A. eexact E. reflexivity.
-  eapply exec_Istore with (a := vaddr'); eauto.
+  eapply exec_Istore with (a := vaddr'). eauto.
   rewrite <- H4. apply eval_addressing_preserved. exact symbols_preserved.
-  traceEq.
+  eauto. traceEq.
   econstructor; eauto. constructor.
 
   (* call *)
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index 5114390..c50c702 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -25,10 +25,6 @@ Require Errors.
 Require Import Maps.
 Require Import AST.
 Require Import Integers.
-Require Import Values.
-Require Import Events.
-Require Import Memory.
-Require Import Globalenvs.
 Require Import Switch.
 Require Import Op.
 Require Import Registers.
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index a14e944..f8dbfe4 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -20,10 +20,8 @@ Require Import Op.
 Require Import Registers.
 Require Import Globalenvs.
 Require Import Values.
-Require Import Memory.
 Require Import Integers.
 Require Import Events.
-Require Import Smallstep.
 Require Import RTL.
 Require Import Conventions.
 
diff --git a/backend/Registers.v b/backend/Registers.v
index fceb7c2..47e10fa 100644
--- a/backend/Registers.v
+++ b/backend/Registers.v
@@ -21,7 +21,6 @@ Require Import Coqlib.
 Require Import AST.
 Require Import Maps.
 Require Import Ordered.
-Require Import FSets.
 Require FSetAVL.
 
 Definition reg: Type := positive.
diff --git a/backend/Reload.v b/backend/Reload.v
index 0ad53e6..31bddcd 100644
--- a/backend/Reload.v
+++ b/backend/Reload.v
@@ -13,11 +13,8 @@
 (** Reloading, spilling, and explication of calling conventions. *)
 
 Require Import Coqlib.
-Require Import Maps.
 Require Import AST.
 Require Import Integers.
-Require Import Values.
-Require Import Globalenvs.
 Require Import Op.
 Require Import Locations.
 Require Import LTLin.
diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v
index 75c7dad..1d49909 100644
--- a/backend/Reloadproof.v
+++ b/backend/Reloadproof.v
@@ -13,7 +13,6 @@
 (** Correctness proof for the [Reload] pass. *)
 
 Require Import Coqlib.
-Require Import Maps.
 Require Import AST.
 Require Import Integers.
 Require Import Values.
@@ -24,7 +23,6 @@ Require Import Smallstep.
 Require Import Op.
 Require Import Locations.
 Require Import Conventions.
-Require Import Allocproof.
 Require Import RTLtyping.
 Require Import LTLin.
 Require Import LTLintyping.
diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v
index eba5ad6..99c89ab 100644
--- a/backend/Reloadtyping.v
+++ b/backend/Reloadtyping.v
@@ -14,7 +14,6 @@
     correctness of computation of stack bounds for Linear. *)
 
 Require Import Coqlib.
-Require Import Maps.
 Require Import AST.
 Require Import Op.
 Require Import Locations.
diff --git a/backend/Renumber.v b/backend/Renumber.v
index b933bba..c862318 100644
--- a/backend/Renumber.v
+++ b/backend/Renumber.v
@@ -15,7 +15,6 @@
 Require Import Coqlib.
 Require Import Maps.
 Require Import Postorder.
-Require Import AST.
 Require Import RTL.
 
 (** CompCert's dataflow analyses (module [Kildall]) are more precise
diff --git a/backend/Renumberproof.v b/backend/Renumberproof.v
index 5ec29e2..d086010 100644
--- a/backend/Renumberproof.v
+++ b/backend/Renumberproof.v
@@ -15,10 +15,7 @@
 Require Import Coqlib.
 Require Import Maps.
 Require Import Postorder.
-Require Import AST.
-Require Import Values.
 Require Import Events.
-Require Import Memory.
 Require Import Globalenvs.
 Require Import Smallstep.
 Require Import Op.
diff --git a/backend/Selection.v b/backend/Selection.v
index ff4d863..29bdabc 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -23,12 +23,8 @@
   The source language is Cminor and the target language is CminorSel. *)
 
 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.
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 2fd9219..09dc0ff 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -16,7 +16,6 @@ Require Import Coqlib.
 Require Import Maps.
 Require Import AST.
 Require Import Integers.
-Require Import Floats.
 Require Import Values.
 Require Import Memory.
 Require Import Events.
diff --git a/backend/Stacking.v b/backend/Stacking.v
index 23a112c..732443b 100644
--- a/backend/Stacking.v
+++ b/backend/Stacking.v
@@ -13,12 +13,10 @@
 (** Layout of activation records; translation from Linear to Mach. *)
 
 Require Import Coqlib.
-Require Import Maps.
 Require Import Errors.
 Require Import AST.
 Require Import Integers.
 Require Import Op.
-Require Import RTL.
 Require Import Locations.
 Require Import Linear.
 Require Import Bounds.
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index 1d87ad3..6c4e43f 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -15,7 +15,6 @@
 (** This file proves semantic preservation for the [Stacking] pass. *)
 
 Require Import Coqlib.
-Require Import Maps.
 Require Import Errors.
 Require Import AST.
 Require Import Integers.
diff --git a/backend/Stackingtyping.v b/backend/Stackingtyping.v
index 27de557..2324cd5 100644
--- a/backend/Stackingtyping.v
+++ b/backend/Stackingtyping.v
@@ -13,7 +13,6 @@
 (** Type preservation for the [Stacking] pass. *)
 
 Require Import Coqlib.
-Require Import Maps.
 Require Import Errors.
 Require Import Integers.
 Require Import AST.
diff --git a/backend/Tailcall.v b/backend/Tailcall.v
index 158002e..917ec83 100644
--- a/backend/Tailcall.v
+++ b/backend/Tailcall.v
@@ -15,7 +15,6 @@
 Require Import Coqlib.
 Require Import Maps.
 Require Import AST.
-Require Import Globalenvs.
 Require Import Registers.
 Require Import Op.
 Require Import RTL.
diff --git a/backend/Tunneling.v b/backend/Tunneling.v
index 8dd1fe2..18414a8 100644
--- a/backend/Tunneling.v
+++ b/backend/Tunneling.v
@@ -16,10 +16,6 @@ Require Import Coqlib.
 Require Import Maps.
 Require Import UnionFind.
 Require Import AST.
-Require Import Values.
-Require Import Globalenvs.
-Require Import Op.
-Require Import Locations.
 Require Import LTL.
 
 (** Branch tunneling shortens sequences of branches (with no intervening
diff --git a/backend/Tunnelingtyping.v b/backend/Tunnelingtyping.v
index 743b468..dfc36b6 100644
--- a/backend/Tunnelingtyping.v
+++ b/backend/Tunnelingtyping.v
@@ -14,13 +14,7 @@
 
 Require Import Coqlib.
 Require Import Maps.
-Require Import UnionFind.
 Require Import AST.
-Require Import Values.
-Require Import Memory.
-Require Import Globalenvs.
-Require Import Op.
-Require Import Locations.
 Require Import LTL.
 Require Import LTLtyping.
 Require Import Tunneling.