4 files changed, 6 insertions, 24 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index c35ba44aa5..912e52cec8 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -782,13 +782,7 @@ end
 let z_two = Z.of_int 2
 
 (** Conversion from bigint to int63 *)
-let rec int63_of_pos_bigint i =
-  if Z.(equal i zero) then Uint63.of_int 0
-  else
-    let quo, remi = Z.div_rem i z_two in
-    if Z.(equal remi one) then Uint63.add (Uint63.of_int 1)
-      (Uint63.mul (Uint63.of_int 2) (int63_of_pos_bigint quo))
-    else Uint63.mul (Uint63.of_int 2) (int63_of_pos_bigint quo)
+let int63_of_pos_bigint i = Uint63.of_int64 (Z.to_int64 i)
 
 module Numbers = struct
 (** * Number notation *)
@@ -1041,7 +1035,7 @@ let interp_int63 ?loc n =
 
 let bigint_of_int63 c =
   match Constr.kind c with
-  | Int i -> Z.of_string (Uint63.to_string i)
+  | Int i -> Z.of_int64 (Uint63.to_int64 i)
   | _ -> raise NotAValidPrimToken
 
 let interp o ?loc n =
diff --git a/kernel/uint63.mli b/kernel/uint63.mli
index 6b47dfc61d..6b2519918a 100644
--- a/kernel/uint63.mli
+++ b/kernel/uint63.mli
@@ -17,6 +17,7 @@ val maxuint31 : t
 val of_int : int -> t
 val to_int2 : t -> int * int (* msb, lsb *)
 val of_int64 : Int64.t -> t
+val to_int64 : t -> Int64.t
 (*
 val of_uint : int -> t
  *)
@@ -32,7 +33,6 @@ val hash : t -> int
 
      (* conversion to a string *)
 val to_string : t -> string
-val of_string : string -> t
 
 val compile : t -> string
 
diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml
index 696efacb32..3517f51bfc 100644
--- a/kernel/uint63_31.ml
+++ b/kernel/uint63_31.ml
@@ -26,6 +26,7 @@ let mask63 i = Int64.logand i maxuint63
 let of_int i = Int64.of_int i
 let to_int2 i = (Int64.to_int (Int64.shift_right_logical i 31), Int64.to_int i)
 let of_int64 i = i
+let to_int64 i = i
 
 let to_int_min n m =
   if Int64.(compare n (of_int m)) < 0 then Int64.to_int n else m
@@ -41,13 +42,6 @@ let hash i =
     (* conversion of an uint63 to a string *)
 let to_string i = Int64.to_string i
 
-let of_string s =
-  let i64 = Int64.of_string s in
-  if Int64.compare Int64.zero i64 <= 0
-      && Int64.compare i64 maxuint63 <= 0
-  then i64
-  else raise (Failure "Int63.of_string")
-
 (* Compiles an unsigned int to OCaml code *)
 let compile i = Printf.sprintf "Uint63.of_int64 (%LiL)" i
 
diff --git a/kernel/uint63_63.ml b/kernel/uint63_63.ml
index 21f57e2bfb..8d052d6593 100644
--- a/kernel/uint63_63.ml
+++ b/kernel/uint63_63.ml
@@ -25,7 +25,8 @@ let of_int i = i
 
 let to_int2 i = (0,i)
 
-let of_int64 _i = assert false
+let of_int64 = Int64.to_int
+let to_int64 = to_uint64
 
 let of_float = int_of_float
 
@@ -39,13 +40,6 @@ let hash i = i
     (* conversion of an uint63 to a string *)
 let to_string i = Int64.to_string (to_uint64 i)
 
-let of_string s =
-  let i64 = Int64.of_string s in
-  if Int64.compare Int64.zero i64 <= 0
-      && Int64.compare i64 maxuint63 <= 0
-  then Int64.to_int i64
-  else raise (Failure "Int64.of_string")
-
 (* Compiles an unsigned int to OCaml code *)
 let compile i = Printf.sprintf "Uint63.of_int (%i)" i