diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-01-29 09:10:29 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-01-29 09:10:29 +0000 |
| commit | 056068abd228fefab4951a61700aa6d54fb88287 (patch) | |
| tree | 6bf44526caf535e464e33999641b39032901fa67 /checklink/Asm_printers.ml | |
| parent | 34d58b781afec8ecd4afdcf2ab83f1c972338ba9 (diff) | |
Ported to Coq 8.4pl1. Merge of branches/coq-8.4.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'checklink/Asm_printers.ml')
| -rw-r--r-- | checklink/Asm_printers.ml | 17 |
1 files changed, 3 insertions, 14 deletions
diff --git a/checklink/Asm_printers.ml b/checklink/Asm_printers.ml index 094d51d..aeb4b3f 100644 --- a/checklink/Asm_printers.ml +++ b/checklink/Asm_printers.ml @@ -1,21 +1,10 @@ +open Camlcoq open Asm open AST -open BinInt -open BinPos open Library -let rec int_of_pos = function - | Coq_xH -> 1 - | Coq_xO q -> 2 * int_of_pos q - | Coq_xI q -> 2 * int_of_pos q + 1 - -let string_of_pos p = string_of_int (int_of_pos p) - -let string_of_coq_Z = function - | Z0 -> "0" - | Zpos p -> string_of_pos p - | Zneg p -> "-" ^ string_of_pos p - +let string_of_pos p = Z.to_string (Z.Zpos p) +let string_of_coq_Z = Z.to_string let string_of_ident = string_of_pos let string_of_label = string_of_pos let string_of_iint = string_of_coq_Z |