Remove some useless "Require".

Update ARM port.


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

6 files changed, 3 insertions, 18 deletions

diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index 4200c11b..b78dfb66 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -13,14 +13,10 @@
 (** Translation from Mach to ARM. *)
 
 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/arm/Asmgenretaddr.v b/arm/Asmgenretaddr.v
index 48b6328c..2d3c72d3 100644
--- a/arm/Asmgenretaddr.v
+++ b/arm/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/arm/ConstpropOp.vp b/arm/ConstpropOp.vp
index 0f06703c..a9cbad5d 100644
--- a/arm/ConstpropOp.vp
+++ b/arm/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/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 0cee7865..64152487 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -640,7 +640,8 @@ let print_instruction oc = function
       | EF_inline_asm txt ->
           fprintf oc "%s begin inline assembly\n" comment;
           fprintf oc "	%s\n" (extern_atom txt);
-          fprintf oc "%s end inline assembly\n" comment
+          fprintf oc "%s end inline assembly\n" comment;
+          5 (* hoping this is an upper bound...  *)
       | _ ->
           assert false
       end
@@ -754,13 +755,13 @@ let print_var oc name v =
       fprintf oc "	.size	%a, . - %a\n" print_symb name print_symb name
 
 let print_globdef oc (name, gdef) =
+  match gdef with
   | Gfun(Internal f) -> print_function oc name f
   | Gfun(External ef) -> ()
   | Gvar v -> print_var oc name v
 
 let print_program oc p =
 (*  fprintf oc "	.fpu	vfp\n"; *)
-  List.iter (print_var oc) p.prog_vars;
   List.iter (print_globdef oc) p.prog_defs
 
 
diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
index 255c97c1..22ef88d2 100644
--- a/arm/SelectOp.vp
+++ b/arm/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/arm/SelectOpproof.v b/arm/SelectOpproof.v
index a72913d3..e25fb0c7 100644
--- a/arm/SelectOpproof.v
+++ b/arm/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.