From d71a5cfd10378301b71d32659d5936e01d72ae50 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 9 May 2010 08:18:51 +0000
Subject: Revised encoding/decoding of floats

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1341 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 arm/PrintAsm.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'arm/PrintAsm.ml')

diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index f5907f40..90b082be 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -14,7 +14,6 @@
 
 open Printf
 open Datatypes
-open Integers
 open Camlcoq
 open AST
 open Asm
@@ -119,7 +118,8 @@ let label_float f =
     max_pos_constants := min !max_pos_constants (!currpos + 1024);
     lbl'
 
-let symbol_labels = (Hashtbl.create 39 : (ident * Int.int, int) Hashtbl.t)
+let symbol_labels =
+  (Hashtbl.create 39 : (ident * Integers.Int.int, int) Hashtbl.t)
 
 let label_symbol id ofs =
   try
-- 
cgit