diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-05-09 08:18:51 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-05-09 08:18:51 +0000 |
| commit | d71a5cfd10378301b71d32659d5936e01d72ae50 (patch) | |
| tree | 9b6a7cc437ab205b7e0bf5bf90585451d8a8c367 /arm | |
| parent | 913c1bcc4b2204afd447edd723e06b905fd1f47f (diff) | |
Revised encoding/decoding of floats
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1341 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'arm')
| -rw-r--r-- | arm/PrintAsm.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index f5907f4..90b082b 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 |