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

4 files changed, 22 insertions, 36 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
diff --git a/checklink/Check.ml b/checklink/Check.ml
index a1cc004..9d668fa 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -1,8 +1,7 @@
+open Camlcoq
 open Asm
 open Asm_printers
 open AST
-open BinInt
-open BinPos
 open Bitstring_utils
 open C2C
 open Camlcoq
@@ -204,7 +203,7 @@ let re_variadic_stub: Str.regexp = Str.regexp "\\(.*\\)\\$[if]*$"
     address, unless the symbol is a stub from CompCert. Otherwise, it filters
     out all symbols whose virtual address does not match [vaddr].
 *)
-let idmap_unify (k: positive) (vaddr: int32) (sfw: s_framework)
+let idmap_unify (k: P.t) (vaddr: int32) (sfw: s_framework)
     : s_framework or_err =
   try (
     (* get the list of possible symbols for ident [k] *)
@@ -438,13 +437,13 @@ let match_csts (cc: constant) (ec: int32): checker = fun ffw ->
       (* sda should be handled separately in places it occurs *)
       fatal "Unhandled Csymbol_sda, please report."
 
-let match_z_int32 (cz: coq_Z) (ei: int32) =
+let match_z_int32 (cz: Z.t) (ei: int32) =
   let cz = z_int32 cz in
   check_eq (
     Printf.sprintf "match_z_int32 %s %s" (string_of_int32 cz) (string_of_int32 ei)
   ) cz ei
 
-let match_z_int (cz: coq_Z) (ei: int) =
+let match_z_int (cz: Z.t) (ei: int) =
   let cz = z_int32 cz in
   let ei = Safe32.of_int ei in
   check_eq (
@@ -452,7 +451,7 @@ let match_z_int (cz: coq_Z) (ei: int) =
   ) cz ei
 
 (* [m] is interpreted as a bitmask, and checked against [ei]. *)
-let match_mask (m: coq_Z) (ei: int32) =
+let match_mask (m: Z.t) (ei: int32) =
   let m = z_int32_lax m in
   check_eq (
     Printf.sprintf "match_mask %s %s"
diff --git a/checklink/Frameworks.ml b/checklink/Frameworks.ml
index 074a432..35144dc 100644
--- a/checklink/Frameworks.ml
+++ b/checklink/Frameworks.ml
@@ -1,6 +1,6 @@
+open Camlcoq
 open Asm
 open AST
-open BinPos
 open ELF_types
 open Lens
 open Library
@@ -62,7 +62,7 @@ type e_framework = {
 }
 
 module PosOT = struct
-  type t = positive
+  type t = P.t
   let compare = Pervasives.compare
 end
 
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)