Merge PR #11742: [numeral] [plugins] Remove Coq's `Bigint` module in favor of ZArith.

Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: liyishuai
Ack-by: MSoegtropIMC
Ack-by: ejgallego
Ack-by: maximedenes
Ack-by: proux01
Ack-by: vbgl

10 files changed, 136 insertions, 131 deletions

diff --git a/plugins/extraction/big.ml b/plugins/extraction/big.ml
index 19055fd425..7228f709f1 100644
--- a/plugins/extraction/big.ml
+++ b/plugins/extraction/big.ml
@@ -8,63 +8,61 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** [Big] : a wrapper around ocaml [Big_int] with nicer names,
+(** [Big] : a wrapper around ocaml [ZArith] with nicer names,
     and a few extraction-specific constructions *)
 
-(** To be linked with [nums.(cma|cmxa)] *)
+(** To be linked with [zarith] *)
 
-open Big_int
-
-type big_int = Big_int.big_int
+type big_int = Z.t
     (** The type of big integers. *)
 
-let zero = zero_big_int
+let zero = Z.zero
         (** The big integer [0]. *)
 
-let one = unit_big_int
+let one = Z.one
         (** The big integer [1]. *)
 
-let two = big_int_of_int 2
+let two = Z.of_int 2
         (** The big integer [2]. *)
 
 (** {6 Arithmetic operations} *)
 
-let opp = minus_big_int
+let opp = Z.neg
         (** Unary negation. *)
 
-let abs = abs_big_int
+let abs = Z.abs
         (** Absolute value. *)
 
-let add = add_big_int
+let add = Z.add
         (** Addition. *)
 
-let succ = succ_big_int
-        (** Successor (add 1). *)
+let succ = Z.succ
+(** Successor (add 1). *)
 
-let add_int = add_int_big_int
+let add_int = Z.add
         (** Addition of a small integer to a big integer. *)
 
-let sub = sub_big_int
+let sub = Z.sub
         (** Subtraction. *)
 
-let pred = pred_big_int
+let pred = Z.pred
         (** Predecessor (subtract 1). *)
 
-let mult = mult_big_int
+let mult = Z.mul
         (** Multiplication of two big integers. *)
 
-let mult_int = mult_int_big_int
+let mult_int x y = Z.mul (Z.of_int x) y
         (** Multiplication of a big integer by a small integer *)
 
-let square = square_big_int
+let square x = Z.mul x x
         (** Return the square of the given big integer *)
 
-let sqrt = sqrt_big_int
+let sqrt = Z.sqrt
         (** [sqrt_big_int a] returns the integer square root of [a],
            that is, the largest big integer [r] such that [r * r <= a].
            Raise [Invalid_argument] if [a] is negative. *)
 
-let quomod = quomod_big_int
+let quomod = Z.div_rem
         (** Euclidean division of two big integers.
            The first part of the result is the quotient,
            the second part is the remainder.
@@ -72,18 +70,18 @@ let quomod = quomod_big_int
            [a = q * b + r] and [0 <= r < |b|].
            Raise [Division_by_zero] if the divisor is zero. *)
 
-let div = div_big_int
+let div = Z.div
         (** Euclidean quotient of two big integers.
            This is the first result [q] of [quomod_big_int] (see above). *)
 
-let modulo = mod_big_int
+let modulo = Z.(mod)
         (** Euclidean modulus of two big integers.
            This is the second result [r] of [quomod_big_int] (see above). *)
 
-let gcd = gcd_big_int
+let gcd = Z.gcd
         (** Greatest common divisor of two big integers. *)
 
-let power = power_big_int_positive_big_int
+let power = Z.pow
         (** Exponentiation functions.  Return the big integer
            representing the first argument [a] raised to the power [b]
            (the second argument).  Depending
@@ -92,45 +90,45 @@ let power = power_big_int_positive_big_int
 
 (** {6 Comparisons and tests} *)
 
-let sign = sign_big_int
+let sign = Z.sign
         (** Return [0] if the given big integer is zero,
            [1] if it is positive, and [-1] if it is negative. *)
 
-let compare = compare_big_int
+let compare = Z.compare
         (** [compare_big_int a b] returns [0] if [a] and [b] are equal,
            [1] if [a] is greater than [b], and [-1] if [a] is smaller
            than [b]. *)
 
-let eq = eq_big_int
-let le = le_big_int
-let ge = ge_big_int
-let lt = lt_big_int
-let gt = gt_big_int
+let eq = Z.equal
+let le = Z.leq
+let ge = Z.geq
+let lt = Z.lt
+let gt = Z.gt
         (** Usual boolean comparisons between two big integers. *)
 
-let max = max_big_int
+let max = Z.max
         (** Return the greater of its two arguments. *)
 
-let min = min_big_int
+let min = Z.min
         (** Return the smaller of its two arguments. *)
 
 (** {6 Conversions to and from strings} *)
 
-let to_string = string_of_big_int
+let to_string = Z.to_string
         (** Return the string representation of the given big integer,
            in decimal (base 10). *)
 
-let of_string = big_int_of_string
+let of_string = Z.of_string
         (** Convert a string to a big integer, in decimal.
            The string consists of an optional [-] or [+] sign,
            followed by one or several decimal digits. *)
 
 (** {6 Conversions to and from other numerical types} *)
 
-let of_int = big_int_of_int
+let of_int = Z.of_int
         (** Convert a small integer to a big integer. *)
 
-let is_int = is_int_big_int
+let is_int = Z.fits_int
         (** Test whether the given big integer is small enough to
            be representable as a small integer (type [int])
            without loss of precision.  On a 32-bit platform,
@@ -139,7 +137,7 @@ let is_int = is_int_big_int
            [is_int_big_int a] returns [true] if and only if
            [a] is between -2{^62} and 2{^62}-1. *)
 
-let to_int = int_of_big_int
+let to_int = Z.to_int
         (** Convert a big integer to a small integer (type [int]).
            Raises [Failure "int_of_big_int"] if the big integer
            is not representable as a small integer. *)
diff --git a/plugins/extraction/dune b/plugins/extraction/dune
index 0c01dcd488..d9d675fe6a 100644
--- a/plugins/extraction/dune
+++ b/plugins/extraction/dune
@@ -2,6 +2,6 @@
  (name extraction_plugin)
  (public_name coq.plugins.extraction)
  (synopsis "Coq's extraction plugin")
- (libraries num coq.plugins.ltac))
+ (libraries coq.plugins.ltac))
 
 (coq.pp (modules g_extraction))
diff --git a/plugins/nsatz/dune b/plugins/nsatz/dune
index b921c9c408..3b67ab3429 100644
--- a/plugins/nsatz/dune
+++ b/plugins/nsatz/dune
@@ -2,6 +2,6 @@
  (name nsatz_plugin)
  (public_name coq.plugins.nsatz)
  (synopsis "Coq's nsatz solver plugin")
- (libraries num coq.plugins.ltac))
+ (libraries coq.plugins.ltac))
 
 (coq.pp (modules g_nsatz))
diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml
index 387145a5d0..cbc1773ede 100644
--- a/plugins/nsatz/ideal.ml
+++ b/plugins/nsatz/ideal.ml
@@ -153,8 +153,8 @@ end
 module Make (P:Polynom.S) = struct
 
   type coef = P.t
-  let coef0 = P.of_num (Num.Int 0)
-  let coef1 = P.of_num (Num.Int 1)
+  let coef0 = P.of_num Q.zero
+  let coef1 = P.of_num Q.one
   let string_of_coef c = "["^(P.to_string c)^"]"
 
 (***********************************************************************
@@ -305,7 +305,7 @@ let mult_t_pol a m p =
   let map (b, m') = (P.multP a b, mult_mon m m') in
   CList.map map p
 
-let coef_of_int x = P.of_num (Num.Int x)
+let coef_of_int x = P.of_num (Q.of_int x)
 
 (* variable i *)
 let gen d i =
diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml
index 29d08fb4ea..f3021f4ee6 100644
--- a/plugins/nsatz/nsatz.ml
+++ b/plugins/nsatz/nsatz.ml
@@ -13,30 +13,20 @@ open Util
 open Constr
 open Tactics
 
-open Num
 open Utile
 
 (***********************************************************************
  Operations on coefficients
 *)
 
-let num_0 = Int 0
-and num_1 = Int 1
-and num_2 = Int 2
-
-let numdom r =
-  let r' = Ratio.normalize_ratio (ratio_of_num r) in
-  num_of_big_int(Ratio.numerator_ratio r'),
-  num_of_big_int(Ratio.denominator_ratio r')
-
 module BigInt = struct
-  open Big_int
+  open Big_int_Z
 
   type t = big_int
   let of_int = big_int_of_int
   let coef0 = of_int 0
-  let of_num = Num.big_int_of_num
-  let to_num = Num.num_of_big_int
+  let of_num = Q.to_bigint
+  let to_num = Q.of_bigint
   let equal = eq_big_int
   let lt = lt_big_int
   let le = le_big_int
@@ -113,7 +103,7 @@ type vname = string
 
 type term =
   | Zero
-  | Const of Num.num
+  | Const of Q.t
   | Var of vname
   | Opp of term
   | Add of term * term
@@ -122,7 +112,7 @@ type term =
   | Pow of term * int
 
 let const n =
-  if eq_num n num_0 then Zero else Const n
+  if Q.(equal zero) n then Zero else Const n
 let pow(p,i) = if Int.equal i 1 then p else Pow(p,i)
 let add = function
     (Zero,q) -> q
@@ -131,8 +121,8 @@ let add = function
 let mul = function
     (Zero,_) -> Zero
   | (_,Zero) -> Zero
-  | (p,Const n) when eq_num n num_1 -> p
-  | (Const n,q) when eq_num n num_1 -> q
+  | (p,Const n) when Q.(equal one) n -> p
+  | (Const n,q) when Q.(equal one) n -> q
   | (p,q) -> Mul(p,q)
 
 let gen_constant n = lazy (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n))
@@ -167,62 +157,64 @@ let mkt_app name l =  mkApp (Lazy.force name, Array.of_list l)
 let tlp () = mkt_app tlist [mkt_app tpexpr [Lazy.force tz]]
 let tllp () = mkt_app tlist [tlp()]
 
-let rec mkt_pos n =
-  if n =/ num_1 then Lazy.force pxH
-  else if mod_num n num_2 =/ num_0 then
-    mkt_app pxO [mkt_pos (quo_num n num_2)]
+let mkt_pos n =
+  let rec mkt_pos n =
+  if Z.(equal one) n then Lazy.force pxH
+  else if Z.is_even n then
+    mkt_app pxO [mkt_pos Z.(n asr 1)]
   else
-    mkt_app pxI [mkt_pos (quo_num n num_2)]
+    mkt_app pxI [mkt_pos Z.(n asr 1)]
+  in mkt_pos (Q.to_bigint n)
 
 let mkt_n n =
-  if Num.eq_num n num_0
+  if Q.(equal zero) n
   then Lazy.force nN0
   else mkt_app nNpos [mkt_pos n]
 
 let mkt_z z  =
-  if z =/ num_0 then  Lazy.force z0
-  else if z >/ num_0 then
+  if Q.(equal zero) z then  Lazy.force z0
+  else if Q.(lt zero) z then
     mkt_app zpos [mkt_pos z]
   else
-    mkt_app zneg [mkt_pos ((Int 0) -/ z)]
+    mkt_app zneg [mkt_pos (Q.neg z)]
 
 let rec mkt_term t  =  match t with
-| Zero -> mkt_term (Const num_0)
-| Const r -> let (n,d) = numdom r in
-  mkt_app  ttconst [Lazy.force tz; mkt_z n]
-| Var v -> mkt_app ttvar [Lazy.force tz; mkt_pos (num_of_string v)]
+| Zero -> mkt_term (Const Q.zero)
+| Const r -> let n = r |> Q.num |> Q.of_bigint in
+  mkt_app ttconst [Lazy.force tz; mkt_z n]
+| Var v -> mkt_app ttvar [Lazy.force tz; mkt_pos (Q.of_string v)]
 | Opp t1 -> mkt_app  ttopp [Lazy.force tz; mkt_term t1]
 | Add (t1,t2) -> mkt_app  ttadd [Lazy.force tz; mkt_term t1; mkt_term t2]
 | Sub (t1,t2) -> mkt_app  ttsub [Lazy.force tz; mkt_term t1; mkt_term t2]
 | Mul (t1,t2) -> mkt_app  ttmul [Lazy.force tz; mkt_term t1; mkt_term t2]
 | Pow (t1,n) ->  if Int.equal n 0 then
-    mkt_app ttconst [Lazy.force tz; mkt_z num_1]
+    mkt_app ttconst [Lazy.force tz; mkt_z Q.one]
 else
-    mkt_app ttpow [Lazy.force tz; mkt_term t1; mkt_n (num_of_int n)]
+    mkt_app ttpow [Lazy.force tz; mkt_term t1; mkt_n (Q.of_int n)]
 
 let rec parse_pos p =
   match Constr.kind p with
 | App (a,[|p2|]) ->
-    if Constr.equal a (Lazy.force pxO) then num_2 */ (parse_pos p2)
-    else num_1 +/ (num_2 */ (parse_pos p2))
-| _ -> num_1
+    if Constr.equal a (Lazy.force pxO) then Q.(mul (of_int 2)) (parse_pos p2)
+    else Q.(add one) Q.(mul (of_int 2) (parse_pos p2))
+| _ -> Q.one
 
 let parse_z z =
   match Constr.kind z with
 | App (a,[|p2|]) ->
-    if Constr.equal a (Lazy.force zpos) then parse_pos p2 else (num_0 -/ (parse_pos p2))
-| _ -> num_0
+    if Constr.equal a (Lazy.force zpos) then parse_pos p2 else Q.neg (parse_pos p2)
+| _ -> Q.zero
 
 let parse_n z =
   match Constr.kind z with
 | App (a,[|p2|]) ->
     parse_pos p2
-| _ -> num_0
+| _ -> Q.zero
 
 let rec parse_term p =
   match Constr.kind p with
 | App (a,[|_;p2|]) ->
-    if Constr.equal a (Lazy.force ttvar) then Var (string_of_num (parse_pos p2))
+    if Constr.equal a (Lazy.force ttvar) then Var (Q.to_string (parse_pos p2))
     else if Constr.equal a (Lazy.force ttconst) then Const (parse_z p2)
     else if Constr.equal a (Lazy.force ttopp) then Opp (parse_term p2)
     else Zero
@@ -231,7 +223,7 @@ let rec parse_term p =
     else if Constr.equal a (Lazy.force ttsub) then Sub (parse_term p2, parse_term p3)
     else if Constr.equal a (Lazy.force ttmul) then Mul (parse_term p2, parse_term p3)
     else if Constr.equal a (Lazy.force ttpow) then
-      Pow (parse_term p2, int_of_num (parse_n p3))
+      Pow (parse_term p2, Q.to_int (parse_n p3))
     else Zero
 | _ -> Zero
 
@@ -278,7 +270,7 @@ let term_pol_sparse nvars np t=
     match t with
     | Zero -> zeroP
     | Const r ->
-        if Num.eq_num r num_0
+        if Q.(equal zero) r
         then zeroP
         else polconst d (Poly.Pint (Coef.of_num r))
     | Var v ->
@@ -316,7 +308,7 @@ let pol_sparse_to_term n2 p =
   let p = PIdeal.repr p in
   let rec aux p =
     match p with
-      [] -> const (num_of_string "0")
+      [] -> const Q.zero
     | (a,m)::p1 ->
       let m = Ideal.Monomial.repr m in
       let n = (Array.length m)-1 in
@@ -443,8 +435,9 @@ let expand_pol lb lp =
 let theoremedeszeros_termes lp =
   let nvars = List.fold_left set_nvars_term 0 lp in
   match lp with
-  | Const (Int sugarparam)::Const (Int nparam)::lp ->
-      ((match sugarparam with
+  | Const sugarparam :: Const nparam :: lp ->
+    let nparam = Q.to_int nparam in
+      ((match Q.to_int sugarparam with
       |0 -> sinfo "computation without sugar";
           lexico:=false;
       |1 -> sinfo "computation with sugar";
diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml
index 726ad54cad..2565d88b13 100644
--- a/plugins/nsatz/polynom.ml
+++ b/plugins/nsatz/polynom.ml
@@ -30,7 +30,7 @@ module type Coef = sig
   val pgcd : t -> t -> t
 
   val hash : t -> int
-  val of_num : Num.num -> t
+  val of_num : Q.t -> t
   val to_string : t -> string
 end
 
@@ -39,7 +39,7 @@ module type S = sig
   type variable = int
   type t = Pint of coef | Prec of variable * t array
 
-  val of_num : Num.num -> t
+  val of_num : Q.t -> t
   val x : variable -> t
   val monome : variable -> int -> t
   val is_constantP : t -> bool
@@ -106,7 +106,7 @@ end
 module Make (C:Coef) = struct
 
 type coef = C.t
-let coef_of_int i = C.of_num (Num.Int i)
+let coef_of_int i = C.of_num (Q.of_int i)
 let coef0 = coef_of_int 0
 let coef1 = coef_of_int 1
 
@@ -125,8 +125,8 @@ type t =
 
 (* constant polynomials *)
 let of_num x = Pint (C.of_num x)
-let cf0 = of_num (Num.Int 0)
-let cf1 = of_num (Num.Int 1)
+let cf0 = of_num Q.zero
+let cf1 = of_num Q.one
 
 (* nth variable *)
 let x n = Prec (n,[|cf0;cf1|])
diff --git a/plugins/nsatz/polynom.mli b/plugins/nsatz/polynom.mli
index 3807a8582b..91f1bcda90 100644
--- a/plugins/nsatz/polynom.mli
+++ b/plugins/nsatz/polynom.mli
@@ -26,7 +26,7 @@ module type Coef = sig
   val pgcd : t -> t -> t
 
   val hash : t -> int
-  val of_num : Num.num -> t
+  val of_num : Q.t -> t
   val to_string : t -> string
 end
 
@@ -35,7 +35,7 @@ module type S = sig
   type variable = int
   type t = Pint of coef | Prec of variable * t array
 
-  val of_num : Num.num -> t
+  val of_num : Q.t -> t
   val x : variable -> t
   val monome : variable -> int -> t
   val is_constantP : t -> bool
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index cd5b747d75..4f7b3fbe74 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -32,7 +32,22 @@ open Tactypes
 open Context.Named.Declaration
 
 module NamedDecl = Context.Named.Declaration
-module OmegaSolver = Omega.MakeOmegaSolver (Bigint)
+
+module ZOmega = struct
+  type bigint = Z.t
+  let equal = Z.equal
+  let less_than = Z.lt
+  let add = Z.add
+  let sub = Z.sub
+  let mult = Z.mul
+  let euclid = Z.div_rem
+  let neg = Z.neg
+  let zero = Z.zero
+  let one = Z.one
+  let to_string = Z.to_string
+end
+
+module OmegaSolver = Omega.MakeOmegaSolver (ZOmega)
 open OmegaSolver
 
 (* Added by JCF, 09/03/98 *)
@@ -719,7 +734,7 @@ let rec shuffle p (t1,t2) =
           Oplus(l2,t')
         else [],Oplus(t1,t2)
     | Oz t1,Oz t2 ->
-        [focused_simpl p], Oz(Bigint.add t1 t2)
+        [focused_simpl p], Oz(Z.add t1 t2)
     | t1,t2 ->
         if weight t1 < weight t2 then
           [clever_rewrite p [[P_APP 1];[P_APP 2]]
@@ -741,7 +756,7 @@ let shuffle_mult p_init k1 e1 k2 e2 =
                               [P_APP 2; P_APP 2]]
               (Lazy.force coq_fast_OMEGA10)
           in
-          if Bigint.add (Bigint.mult k1 c1) (Bigint.mult k2 c2) =? zero then
+          if Z.add (Z.mul k1 c1) (Z.mul k2 c2) =? zero then
             let tac' =
               clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]]
                 (Lazy.force coq_fast_Zred_factor5) in
@@ -798,7 +813,7 @@ let shuffle_mult_right p_init e1 k2 e2 =
                [P_APP 2; P_APP 2]]
               (Lazy.force coq_fast_OMEGA15)
           in
-          if Bigint.add c1 (Bigint.mult k2 c2) =? zero then
+          if Z.add c1 (Z.mul k2 c2) =? zero then
             let tac' =
               clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]]
                 (Lazy.force coq_fast_Zred_factor5)
@@ -1004,7 +1019,7 @@ let reduce_factor p = function
   | Otimes(Oatom v,c) ->
       let rec compute = function
         | Oz n -> n
-        | Oplus(t1,t2) -> Bigint.add (compute t1) (compute t2)
+        | Oplus(t1,t2) -> Z.add (compute t1) (compute t2)
         | _ -> CErrors.user_err Pp.(str "condense.1")
       in
       [focused_simpl (P_APP 2 :: p)], Otimes(Oatom v,Oz(compute c))
@@ -1160,7 +1175,7 @@ let replay_history tactic_normalisation =
 
       | NOT_EXACT_DIVIDE (e1,k) :: l ->
           let c = floor_div e1.constant k in
-          let d = Bigint.sub e1.constant (Bigint.mult c k) in
+          let d = Z.sub e1.constant (Z.mul c k) in
           let e2 =  {id=e1.id; kind=EQUA;constant = c;
                      body = map_eq_linear (fun c -> c / k) e1.body } in
           let eq2 = val_of(decompile e2) in
diff --git a/plugins/syntax/float_syntax.ml b/plugins/syntax/float_syntax.ml
index 8e87fc13ca..5d8dcd04fe 100644
--- a/plugins/syntax/float_syntax.ml
+++ b/plugins/syntax/float_syntax.ml
@@ -48,21 +48,21 @@ let interp_float ?loc n =
            | None -> "" | Some f -> NumTok.UnsignedNat.to_string f in
          let e = match e with
            | None -> "0" | Some e -> NumTok.SignedNat.to_string e in
-         Bigint.of_string (i ^ f),
+         Z.of_string (i ^ f),
          (try int_of_string e with Failure _ -> 0) - String.length f in
        let m', e' =
          let m', e' = Float64.frshiftexp f in
          let m' = Float64.normfr_mantissa m' in
          let e' = Uint63.to_int_min e' 4096 - Float64.eshift - 53 in
-         Bigint.of_string (Uint63.to_string m'),
+         Z.of_string (Uint63.to_string m'),
          e' in
-       let c2, c5 = Bigint.(of_int 2, of_int 5) in
+       let c2, c5 = Z.(of_int 2, of_int 5) in
        (* check m*5^e <> m'*2^e' *)
        let check m e m' e' =
-         not (Bigint.(equal (mult m (pow c5 e)) (mult m' (pow c2 e')))) in
+         not (Z.(equal (mul m (pow c5 e)) (mul m' (pow c2 e')))) in
        (* check m*5^e*2^e' <> m' *)
        let check' m e e' m' =
-         not (Bigint.(equal (mult (mult m (pow c5 e)) (pow c2 e')) m')) in
+         not (Z.(equal (mul (mul m (pow c5 e)) (pow c2 e')) m')) in
        (* we now have to check m*10^e <> m'*2^e' *)
        if e >= 0 then
          if e <= e' then check m e m' (e' - e)
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 23a7cc07c5..d66b9537b4 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -11,7 +11,6 @@
 open Util
 open Names
 open Glob_term
-open Bigint
 
 (* Poor's man DECLARE PLUGIN *)
 let __coq_plugin_name = "r_syntax_plugin"
@@ -47,10 +46,10 @@ let pos_of_bignat ?loc x =
   let ref_xH = DAst.make @@ GRef (glob_xH, None) in
   let ref_xO = DAst.make @@ GRef (glob_xO, None) in
   let rec pos_of x =
-    match div2_with_rest x with
-      | (q,false) -> DAst.make @@ GApp (ref_xO,[pos_of q])
-      | (q,true) when not (Bigint.equal q zero) -> DAst.make @@ GApp (ref_xI,[pos_of q])
-      | (q,true) -> ref_xH
+    match Z.(div_rem x (of_int 2)) with
+      | (q,rem) when rem = Z.zero -> DAst.make @@ GApp (ref_xO,[pos_of q])
+      | (q,_) when not Z.(equal q zero) -> DAst.make @@ GApp (ref_xI,[pos_of q])
+      | (q,_) -> ref_xH
   in
   pos_of x
 
@@ -59,9 +58,9 @@ let pos_of_bignat ?loc x =
 (**********************************************************************)
 
 let rec bignat_of_pos c = match DAst.get c with
-  | GApp (r, [a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a)
-  | GApp (r, [a]) when is_gr r glob_xI -> add_1(mult_2(bignat_of_pos a))
-  | GRef (a, _) when GlobRef.equal a glob_xH -> Bigint.one
+  | GApp (r, [a]) when is_gr r glob_xO -> Z.mul Z.(of_int 2) (bignat_of_pos a)
+  | GApp (r, [a]) when is_gr r glob_xI -> Z.add Z.one Z.(mul (of_int 2) (bignat_of_pos a))
+  | GRef (a, _) when GlobRef.equal a glob_xH -> Z.one
   | _ -> raise Non_closed_number
 
 (**********************************************************************)
@@ -77,9 +76,9 @@ let glob_POS = GlobRef.ConstructRef path_of_POS
 let glob_NEG = GlobRef.ConstructRef path_of_NEG
 
 let z_of_int ?loc n =
-  if not (Bigint.equal n zero) then
+  if not Z.(equal n zero) then
     let sgn, n =
-      if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in
+      if Z.(leq zero n) then glob_POS, n else glob_NEG, Z.neg n in
     DAst.make @@ GApp(DAst.make @@ GRef (sgn,None), [pos_of_bignat ?loc n])
   else
     DAst.make @@ GRef (glob_ZERO, None)
@@ -90,8 +89,8 @@ let z_of_int ?loc n =
 
 let bigint_of_z c = match DAst.get c with
   | GApp (r,[a]) when is_gr r glob_POS -> bignat_of_pos a
-  | GApp (r,[a]) when is_gr r glob_NEG -> Bigint.neg (bignat_of_pos a)
-  | GRef (a, _) when GlobRef.equal a glob_ZERO -> Bigint.zero
+  | GApp (r,[a]) when is_gr r glob_NEG -> Z.neg (bignat_of_pos a)
+  | GRef (a, _) when GlobRef.equal a glob_ZERO -> Z.zero
   | _ -> raise Non_closed_number
 
 (**********************************************************************)
@@ -122,13 +121,13 @@ let r_of_rawnum ?loc n =
   let rdiv r r' =
     DAst.make @@ GApp (DAst.make @@ GRef(glob_Rdiv,None), [r; r']) in
   let pow p e =
-    let p = z_of_int ?loc (Bigint.of_int p) in
+    let p = z_of_int ?loc (Z.of_int p) in
     let e = pos_of_bignat e in
     DAst.make @@ GApp (DAst.make @@ GRef(glob_pow_pos,None), [p; e]) in
   let n =
     izr (z_of_int ?loc n) in
-  if Bigint.is_strictly_pos e then rmult n (izr (pow p e))
-  else if Bigint.is_strictly_neg e then rdiv n (izr (pow p (neg e)))
+  if Int.equal (Z.sign e) 1 then rmult n (izr (pow p e))
+  else if Int.equal (Z.sign e) (-1) then rdiv n (izr (pow p (Z.neg e)))
   else n  (* e = 0 *)
 
 (**********************************************************************)
@@ -141,24 +140,24 @@ let rawnum_of_r c =
     (* choose between 123e-2 and 1.23, this is purely heuristic
        and doesn't play any soundness role *)
     let choose_exponent =
-      if Bigint.is_strictly_pos e then
+      if Int.equal (Z.sign e) 1 then
         true  (* don't print 12 * 10^2 as 1200 to distinguish them *)
       else
-        let i = Bigint.to_string i in
+        let i = Z.to_string i in
         let li = if i.[0] = '-' then String.length i - 1 else String.length i in
-        let e = Bigint.neg e in
-        let le = String.length (Bigint.to_string e) in
-        Bigint.(less_than (add (of_int li) (of_int le)) e) in
+        let e = Z.neg e in
+        let le = String.length (Z.to_string e) in
+        Z.(lt (add (of_int li) (of_int le)) e) in
     (* print 123 * 10^-2 as 123e-2 *)
     let numTok_exponent () =
       NumTok.Signed.of_bigint_and_exponent i (NumTok.EDec e) in
     (* print 123 * 10^-2 as 1.23, precondition e < 0 *)
     let numTok_dot () =
       let s, i =
-        if Bigint.is_pos_or_zero i then NumTok.SPlus, Bigint.to_string i
-        else NumTok.SMinus, Bigint.(to_string (neg i)) in
+        if Z.sign i >= 0 then NumTok.SPlus, Z.to_string i
+        else NumTok.SMinus, Z.(to_string (neg i)) in
       let ni = String.length i in
-      let e = - (Bigint.to_int e) in
+      let e = - (Z.to_int e) in
       assert (e > 0);
       let i, f =
         if e < ni then String.sub i 0 (ni - e), String.sub i (ni - e) e
@@ -178,12 +177,12 @@ let rawnum_of_r c =
         begin match DAst.get r with
         | GApp (p, [t; e]) when is_gr p glob_pow_pos ->
            let t = bigint_of_z t in
-           if not (Bigint.(equal t (of_int 10))) then
+           if not (Z.(equal t (of_int 10))) then
              raise Non_closed_number
            else
              let i = bigint_of_z l in
              let e = bignat_of_pos e in
-             let e = if is_gr md glob_Rdiv then neg e else e in
+             let e = if is_gr md glob_Rdiv then Z.neg e else e in
              numTok_of_int_exp i e
         | _ -> raise Non_closed_number
         end