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
---
 arm/PrintAsm.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'arm/PrintAsm.ml')

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