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/Library.ml | 26 ++++++++++++--------------
 1 file changed, 12 insertions(+), 14 deletions(-)

(limited to 'checklink/Library.ml')

diff --git a/checklink/Library.ml b/checklink/Library.ml
index c38c1f1..acea80a 100644
--- a/checklink/Library.ml
+++ b/checklink/Library.ml
@@ -1,5 +1,3 @@
-open BinInt
-open BinPos
 open Camlcoq
 
 type bitstring = Bitstring.bitstring
@@ -75,9 +73,9 @@ exception Int32Overflow
 (* Can only return positive numbers 0 <= res < 2^31 *)
 let positive_int32 p =
   let rec positive_int32_unsafe = function
-  | Coq_xI(p) -> Int32.(add (shift_left (positive_int32_unsafe p) 1) 1l)
-  | Coq_xO(p) -> Int32.(shift_left (positive_int32_unsafe p) 1)
-  | Coq_xH    -> 1l
+  | P.Coq_xI(p) -> Int32.(add (shift_left (positive_int32_unsafe p) 1) 1l)
+  | P.Coq_xO(p) -> Int32.(shift_left (positive_int32_unsafe p) 1)
+  | P.Coq_xH    -> 1l
   in
   let res = positive_int32_unsafe p in
   if res >= 0l
@@ -86,27 +84,27 @@ let positive_int32 p =
 
 (* This allows for 1 bit of overflow, effectively returning a negative *)
 let rec positive_int32_lax = function
-| Coq_xI(p) ->
+| P.Coq_xI(p) ->
     let acc = positive_int32_lax p in
     if acc < 0l
     then raise Int32Overflow
     else Int32.(add (shift_left acc 1) 1l)
-| Coq_xO(p) ->
+| P.Coq_xO(p) ->
     let acc = positive_int32_lax p in
     if acc < 0l
     then raise Int32Overflow
     else Int32.shift_left acc 1
-| Coq_xH -> 1l
+| P.Coq_xH -> 1l
 
 let z_int32 = function
-| Z0      -> 0l
-| Zpos(p) -> positive_int32 p
-| Zneg(p) -> Int32.neg (positive_int32 p)
+| Z.Z0      -> 0l
+| Z.Zpos(p) -> positive_int32 p
+| Z.Zneg(p) -> Int32.neg (positive_int32 p)
 
 let z_int32_lax = function
-| Z0      -> 0l
-| Zpos(p) -> positive_int32_lax p
-| Zneg(_) -> raise Int32Overflow
+| Z.Z0      -> 0l
+| Z.Zpos(p) -> positive_int32_lax p
+| Z.Zneg(_) -> raise Int32Overflow
 
 let z_int z = Safe32.to_int (z_int32 z)
 
-- 
cgit v1.2.3