From 056068abd228fefab4951a61700aa6d54fb88287 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Tue, 29 Jan 2013 09:10:29 +0000
Subject: 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
---
 checklink/Asm_printers.ml | 17 +++--------------
 1 file changed, 3 insertions(+), 14 deletions(-)

(limited to 'checklink/Asm_printers.ml')

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
-- 
cgit v1.2.3