[numeral] [plugins] Switch from `Big_int` to ZArith.

We replace Coq's use of `Big_int` and `num` by the ZArith OCaml
library which is a more modern version.

We switch the core files and easy plugins only for now, more complex
numerical plugins will be done in their own commit.

We thus keep the num library linked for now until all plugins are
ported.

Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>

33 files changed, 203 insertions, 739 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 51d39936d0..cc8a4d34c9 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -19,7 +19,7 @@ stages:
 variables:
   # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
   # for reference]
-  CACHEKEY: "bionic_coq-V2020-08-18-V29"
+  CACHEKEY: "bionic_coq-V2020-08-28-V92"
   IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
   # By default, jobs run in the base switch; override to select another switch
   OPAM_SWITCH: "base"
@@ -600,7 +600,7 @@ test-suite:edge:dune:dev:
     - opam repo add ocaml-beta https://github.com/ocaml/ocaml-beta-repository.git
     - opam update
     - opam install ocaml-variants=$OCAMLVER
-    - opam install dune num
+    - opam install dune num zarith
     - eval $(opam env)
     - export COQ_UNIT_TEST=noop
     - make -f Makefile.dune test-suite
diff --git a/INSTALL.md b/INSTALL.md
index c44c3dde7d..2b5986ded4 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -12,6 +12,8 @@ To compile Coq yourself, you need:
 - The [num](https://github.com/ocaml/num) library; note that it is
   included in the OCaml distribution for OCaml versions < 4.06.0
 
+- The [ZArith library](https://github.com/ocaml/Zarith) >= 1.8
+
 - The [findlib](http://projects.camlcity.org/projects/findlib.html) library (version >= 1.8.0)
 
 - GNU Make (version >= 3.81)
diff --git a/META.coq.in b/META.coq.in
index 883a7286e4..5aaa8cc8a6 100644
--- a/META.coq.in
+++ b/META.coq.in
@@ -120,7 +120,7 @@ package "interp" (
   description = "Coq Term Interpretation"
   version     = "8.13"
 
-  requires    = "coq.pretyping"
+  requires    = "zarith, coq.pretyping"
   directory   = "interp"
 
   archive(byte)    = "interp.cma"
@@ -327,7 +327,7 @@ package "plugins" (
     description = "Coq micromega plugin"
     version     = "8.13"
 
-    requires    = "num,coq.plugins.ltac"
+    requires    = "num, coq.plugins.ltac"
     directory   = "micromega"
 
     archive(byte)    = "micromega_plugin.cmo"
@@ -462,7 +462,7 @@ package "plugins" (
     description = "Coq nsatz plugin"
     version     = "8.13"
 
-    requires    = "num,coq.plugins.ltac"
+    requires    = "zarith, coq.plugins.ltac"
     directory   = "nsatz"
 
     archive(byte)    = "nsatz_plugin.cmo"
diff --git a/Makefile.build b/Makefile.build
index 4fb4b12be2..da3b44b608 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -245,7 +245,7 @@ COQOPTS=$(NATIVECOMPUTE) $(COQWARNERROR) $(COQUSERFLAGS)
 BOOTCOQC=$(TIMER) $(COQC) -coqlib . -q $(COQOPTS)
 
 LOCALINCLUDES=$(addprefix -I ,$(SRCDIRS))
-MLINCLUDES=$(LOCALINCLUDES)
+MLINCLUDES=$(LOCALINCLUDES) -package zarith
 
 USERCONTRIBINCLUDES=$(addprefix -I user-contrib/,$(USERCONTRIBDIRS))
 
@@ -302,7 +302,7 @@ $(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ -linkpkg $(1) $^
 endef
 
 # Main packages linked by Coq.
-SYSMOD:=-package num,str,unix,dynlink,threads
+SYSMOD:=-package str,unix,dynlink,threads,num,zarith
 
 ###########################################################################
 # Infrastructure for the rest of the Makefile
diff --git a/azure-pipelines.yml b/azure-pipelines.yml
index b27d1df39d..5830095861 100644
--- a/azure-pipelines.yml
+++ b/azure-pipelines.yml
@@ -22,7 +22,7 @@ jobs:
       powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/setup-x86_64.exe', 'setup-x86_64.exe')"
       SET CYGROOT=C:\cygwin64
       SET CYGCACHE=%CYGROOT%\var\cache\setup
-      setup-x86_64.exe -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time -P wget -P curl -P git -P mingw64-x86_64-binutils,mingw64-x86_64-gcc-core,mingw64-x86_64-gcc-g++,mingw64-x86_64-pkg-config,mingw64-x86_64-windows_default_manifest -P mingw64-x86_64-headers,mingw64-x86_64-runtime,mingw64-x86_64-pthreads,mingw64-x86_64-zlib -P python3
+      setup-x86_64.exe -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time -P wget -P curl -P git -P mingw64-x86_64-binutils,mingw64-x86_64-gcc-core,mingw64-x86_64-gcc-g++,mingw64-x86_64-pkg-config,mingw64-x86_64-windows_default_manifest -P mingw64-x86_64-headers,mingw64-x86_64-runtime,mingw64-x86_64-pthreads,mingw64-x86_64-zlib,mingw64-x86_64-gmp -P python3
 
       SET TARGET_ARCH=x86_64-w64-mingw32
       SET CD_MFMT=%cd:\=/%
@@ -64,7 +64,7 @@ jobs:
       set -e
       brew update
       (cd $(brew --repository)/Library/Taps/homebrew/homebrew-core/ && git fetch --shallow-since=${HBCORE_DATE} && git checkout ${HBCORE_REF})
-      brew install gnu-time opam pkg-config gtksourceview3 adwaita-icon-theme || true
+      brew install gnu-time opam pkg-config gtksourceview3 adwaita-icon-theme gmp || true
       # || true: workaround #12657, see also #12672 and commit message for this line
       pip3 install macpack
     displayName: 'Install system dependencies'
@@ -80,7 +80,7 @@ jobs:
       opam switch set ocaml-base-compiler.$COMPILER
       eval $(opam env)
       opam update
-      opam install -j "$NJOBS" num ocamlfind${FINDLIB_VER} ounit lablgtk3-sourceview3
+      opam install -j "$NJOBS" num ocamlfind${FINDLIB_VER} ounit lablgtk3-sourceview3 zarith.1.9.1
       opam list
     displayName: 'Install OCaml dependencies'
     env:
diff --git a/clib/bigint.ml b/clib/bigint.ml
deleted file mode 100644
index 735ff3261e..0000000000
--- a/clib/bigint.ml
+++ /dev/null
@@ -1,526 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(***************************************************)
-(* Basic operations on (unbounded) integer numbers *)
-(***************************************************)
-
-(* An integer is canonically represented as an array of k-digits blocs,
-   i.e. in base 10^k.
-
-   0 is represented by the empty array and -1 by the singleton [|-1|].
-   The first bloc is in the range ]0;base[ for positive numbers.
-   The first bloc is in the range [-base;-1[ for numbers < -1.
-   All other blocs are numbers in the range [0;base[.
-
-   Negative numbers are represented using 2's complementation :
-   one unit is "borrowed" from the top block for complementing
-   the other blocs. For instance, with 4-digits blocs,
-   [|-5;6789|] denotes -43211
-   since -5.10^4+6789=-((4.10^4)+(10000-6789)) = -43211
-
-   The base is a power of 10 in order to facilitate the parsing and printing
-   of numbers in digital notation.
-
-   All functions, to the exception of to_string and of_string should work
-   with an arbitrary base, even if not a power of 10.
-
-   In practice, we set k=4 on 32-bits machines, so that no overflow in ocaml
-   machine words (i.e. the interval [-2^30;2^30-1]) occur when multiplying two
-   numbers less than (10^k). On 64-bits machines, k=9.
-*)
-
-(* The main parameters *)
-
-let size =
-  let rec log10 n = if n < 10 then 0 else 1 + log10 (n / 10) in
-  (log10 max_int) / 2
-
-let format_size =
-  (* How to parametrize a printf format *)
-  if Int.equal size 4 then Printf.sprintf "%04d"
-  else if Int.equal size 9 then Printf.sprintf "%09d"
-  else fun n ->
-    let rec aux j l n =
-      if Int.equal j size then l else aux (j+1) (string_of_int (n mod 10) :: l) (n/10)
-    in String.concat "" (aux 0 [] n)
-
-(* The base is 10^size *)
-let base =
-  let rec exp10 = function 0 -> 1 | n -> 10 * exp10 (n-1) in exp10 size
-
-(******************************************************************)
-(* First, we represent all numbers by int arrays.
-   Later, we will optimize the particular case of small integers  *)
-(******************************************************************)
-
-module ArrayInt = struct
-
-(* Basic numbers *)
-let zero = [||]
-
-let is_zero = function
-| [||] -> true
-| _ -> false
-
-(* An array is canonical when
-   - it is empty
-   - it is [|-1|]
-   - its first bloc is in [-base;-1[U]0;base[
-     and the other blocs are in [0;base[. *)
-(*
-let canonical n =
-  let ok x = (0 <= x && x < base) in
-  let rec ok_tail k = (Int.equal k 0) || (ok n.(k) && ok_tail (k-1)) in
-  let ok_init x = (-base <= x && x < base && not (Int.equal x (-1)) && not (Int.equal x 0))
-  in
-  (is_zero n) || (match n with [|-1|] -> true | _ -> false) ||
-    (ok_init n.(0) && ok_tail (Array.length n - 1))
-*)
-
-(* [normalize_pos] : removing initial blocks of 0 *)
-
-let normalize_pos n =
-  let k = ref 0 in
-  while !k < Array.length n && Int.equal n.(!k) 0 do incr k done;
-  Array.sub n !k (Array.length n - !k)
-
-(* [normalize_neg] : avoid (-1) as first bloc.
-   input: an array with -1 as first bloc and other blocs in [0;base[
-   output: a canonical array *)
-
-let normalize_neg n =
-  let k = ref 1 in
-  while !k < Array.length n && Int.equal n.(!k) (base - 1) do incr k done;
-  let n' = Array.sub n !k (Array.length n - !k) in
-  if Int.equal (Array.length n') 0 then [|-1|] else (n'.(0) <- n'.(0) - base; n')
-
-(* [normalize] : avoid 0 and (-1) as first bloc.
-   input: an array with first bloc in [-base;base[ and others in [0;base[
-   output: a canonical array *)
-
-let normalize n =
-  if Int.equal (Array.length n) 0 then n
-  else if Int.equal n.(0) (-1) then normalize_neg n
-  else if Int.equal n.(0) 0 then normalize_pos n
-  else n
-
-(* Opposite (expects and returns canonical arrays) *)
-
-let neg m =
-  if is_zero m then zero else
-  let n = Array.copy m in
-  let i = ref (Array.length m - 1) in
-  while !i > 0 && Int.equal n.(!i) 0 do decr i done;
-  if Int.equal !i 0 then begin
-    n.(0) <- - n.(0);
-    (* n.(0) cannot be 0 since m is canonical *)
-    if Int.equal n.(0) (-1) then normalize_neg n
-    else if Int.equal n.(0) base then (n.(0) <- 0; Array.append [| 1 |] n)
-    else n
-  end else begin
-    (* here n.(!i) <> 0, hence 0 < base - n.(!i) < base for n canonical *)
-    n.(!i) <- base - n.(!i); decr i;
-    while !i > 0 do n.(!i) <- base - 1 - n.(!i); decr i done;
-    (* since -base <= n.(0) <= base-1, hence -base <= -n.(0)-1 <= base-1 *)
-    n.(0) <- - n.(0) - 1;
-    (* since m is canonical, m.(0)<>0 hence n.(0)<>-1,
-       and m=-1 is already handled above, so here m.(0)<>-1 hence n.(0)<>0 *)
-    n
-  end
-
-let push_carry r j =
-  let j = ref j in
-  while !j > 0 && r.(!j) < 0 do
-    r.(!j) <- r.(!j) + base; decr j; r.(!j) <- r.(!j) - 1
-  done;
-  while !j > 0 && r.(!j) >= base do
-    r.(!j) <- r.(!j) - base; decr j; r.(!j) <- r.(!j) + 1
-  done;
-  (* here r.(0) could be in [-2*base;2*base-1] *)
-  if r.(0) >= base then (r.(0) <- r.(0) - base; Array.append [| 1 |] r)
-  else if r.(0) < -base then (r.(0) <- r.(0) + 2*base; Array.append [| -2 |] r)
-  else normalize r (* in case r.(0) is 0 or -1 *)
-
-let add_to r a j =
-  if is_zero a then r else begin
-  for i = Array.length r - 1 downto j+1 do
-    r.(i) <- r.(i) + a.(i-j);
-    if r.(i) >= base then (r.(i) <- r.(i) - base; r.(i-1) <- r.(i-1) + 1)
-  done;
-  r.(j) <- r.(j) + a.(0);
-  push_carry r j
-  end
-
-let add n m =
-  let d = Array.length n - Array.length m in
-  if d > 0 then add_to (Array.copy n) m d else add_to (Array.copy m) n (-d)
-
-let sub_to r a j =
-  if is_zero a then r else begin
-  for i = Array.length r - 1 downto j+1 do
-    r.(i) <- r.(i) - a.(i-j);
-    if r.(i) < 0 then (r.(i) <- r.(i) + base; r.(i-1) <- r.(i-1) - 1)
-  done;
-  r.(j) <- r.(j) - a.(0);
-  push_carry r j
-  end
-
-let sub n m =
-  let d = Array.length n - Array.length m in
-  if d >= 0 then sub_to (Array.copy n) m d
-  else let r = neg m in add_to r n (Array.length r - Array.length n)
-
-let mult m n =
-  if is_zero m || is_zero n then zero else
-  let l = Array.length m + Array.length n in
-  let r = Array.make l 0 in
-  for i = Array.length m - 1 downto 0 do
-    for j = Array.length n - 1 downto 0 do
-      let p = m.(i) * n.(j) + r.(i+j+1) in
-      let (q,s) =
-        if p < 0
-        then (p + 1) / base - 1, (p + 1) mod base + base - 1
-        else p / base, p mod base in
-      r.(i+j+1) <- s;
-      if not (Int.equal q 0) then r.(i+j) <- r.(i+j) + q;
-    done
-  done;
-  normalize r
-
-(* Comparisons *)
-
-let is_strictly_neg n = not (is_zero n) && n.(0) < 0
-let is_strictly_pos n = not (is_zero n) && n.(0) > 0
-let is_neg_or_zero n = is_zero n || n.(0) < 0
-let is_pos_or_zero n = is_zero n || n.(0) > 0
-
-(* Is m without its i first blocs less then n without its j first blocs ?
-   Invariant : |m|-i = |n|-j *)
-
-let rec less_than_same_size m n i j =
-  i < Array.length m &&
-  (m.(i) < n.(j) || (Int.equal m.(i) n.(j) && less_than_same_size m n (i+1) (j+1)))
-
-let less_than m n =
-  if is_strictly_neg m then
-    is_pos_or_zero n || Array.length m > Array.length n
-      || (Int.equal (Array.length m) (Array.length n) && less_than_same_size m n 0 0)
-  else
-    is_strictly_pos n && (Array.length m < Array.length n ||
-    (Int.equal (Array.length m) (Array.length n) && less_than_same_size m n 0 0))
-
-(* For this equality test it is critical that n and m are canonical *)
-
-let rec array_eq len v1 v2 i =
-  if Int.equal len i then true
-  else
-    Int.equal v1.(i) v2.(i) && array_eq len v1 v2 (succ i)
-
-let equal m n =
-  let lenm = Array.length m in
-  let lenn = Array.length n in
-  (Int.equal lenm lenn) && (array_eq lenm m n 0)
-
-(* Is m without its k top blocs less than n ? *)
-
-let less_than_shift_pos k m n =
-  (Array.length m - k < Array.length n)
-  || (Int.equal (Array.length m - k) (Array.length n) && less_than_same_size m n k 0)
-
-let rec can_divide k m d i =
-  (Int.equal i (Array.length d)) ||
-  (m.(k+i) > d.(i)) ||
-  (Int.equal m.(k+i) d.(i) && can_divide k m d (i+1))
-
-(* For two big nums m and d and a small number q,
-   computes m - d * q * base^(|m|-|d|-k) in-place (in m).
-   Both m d and q are positive. *)
-
-let sub_mult m d q k =
-  if not (Int.equal q 0) then
-  for i = Array.length d - 1 downto 0 do
-    let v = d.(i) * q in
-    m.(k+i) <- m.(k+i) - v mod base;
-    if m.(k+i) < 0 then (m.(k+i) <- m.(k+i) + base; m.(k+i-1) <- m.(k+i-1) -1);
-    if v >= base then begin
-      m.(k+i-1) <- m.(k+i-1) - v / base;
-      let j = ref (i-1) in
-      while m.(k + !j) < 0 do (* result is positive, hence !j remains >= 0 *)
-        m.(k + !j) <- m.(k + !j) + base; decr j; m.(k + !j) <- m.(k + !j) -1
-      done
-    end
-  done
-
-(** Euclid division m/d = (q,r), with m = q*d+r and |r|<|q|.
-    This is the "Trunc" variant (a.k.a "Truncated-Toward-Zero"),
-    as with ocaml's / (but not as ocaml's Big_int.quomod_big_int).
-    We have sign r = sign m *)
-
-let euclid m d =
-  let isnegm, m =
-    if is_strictly_neg m then (-1),neg m else 1,Array.copy m in
-  let isnegd, d = if is_strictly_neg d then (-1),neg d else 1,d in
-  if is_zero d then raise Division_by_zero;
-  let q,r =
-    if less_than m d then (zero,m) else
-    let ql = Array.length m - Array.length d in
-    let q = Array.make (ql+1) 0 in
-    let i = ref 0 in
-    while not (less_than_shift_pos !i m d) do
-      if Int.equal m.(!i) 0 then incr i else
-      if can_divide !i m d 0 then begin
-        let v =
-          if Array.length d > 1 && not (Int.equal d.(0) m.(!i)) then
-            (m.(!i) * base + m.(!i+1)) / (d.(0) * base + d.(1) + 1)
-          else
-            m.(!i) / d.(0) in
-        q.(!i) <- q.(!i) + v;
-        sub_mult m d v !i
-      end else begin
-        let v = (m.(!i) * base + m.(!i+1)) / (d.(0) + 1) in
-        q.(!i) <- q.(!i) + v / base;
-        sub_mult m d (v / base) !i;
-        q.(!i+1) <- q.(!i+1) + v mod base;
-        if q.(!i+1) >= base then
-          (q.(!i+1) <- q.(!i+1)-base; q.(!i) <- q.(!i)+1);
-        sub_mult m d (v mod base) (!i+1)
-      end
-    done;
-    (normalize q, normalize m) in
-  (if Int.equal (isnegd * isnegm) (-1) then neg q else q),
-  (if Int.equal isnegm (-1) then neg r else r)
-
-(* Parsing/printing ordinary 10-based numbers *)
-
-let of_string s =
-  let len = String.length s in
-  let isneg = len > 1 && s.[0] == '-' in
-  let d = ref (if isneg then 1 else 0) in
-  while !d < len && s.[!d] == '0' do incr d done;
-  if Int.equal !d len then zero else
-  let r = (len - !d) mod size in
-  let h = String.sub s (!d) r in
-  let e = match h with "" -> 0 | _ -> 1 in
-  let l = (len - !d) / size in
-  let a = Array.make (l + e) 0 in
-  if Int.equal e 1 then a.(0) <- int_of_string h;
-  for i = 1 to l do
-    a.(i+e-1) <- int_of_string (String.sub s ((i-1)*size + !d + r) size)
-  done;
-  if isneg then neg a else a
-
-let to_string_pos sgn n =
-   if Int.equal (Array.length n) 0 then "0" else
-     sgn ^
-     String.concat ""
-      (string_of_int n.(0) :: List.map format_size (List.tl (Array.to_list n)))
-
-let to_string n =
-  if is_strictly_neg n then to_string_pos "-" (neg n)
-  else to_string_pos "" n
-
-end
-
-(******************************************************************)
-(* Optimized operations on (unbounded) integer numbers            *)
-(* integers smaller than base are represented as machine integers *)
-(******************************************************************)
-
-open ArrayInt
-
-type bigint = Obj.t
-
-(* Since base is the largest power of 10 such that base*base <= max_int,
-   we have max_int < 100*base*base : any int can be represented
-   by at most three blocs *)
-
-let small n = (-base <= n) && (n < base)
-
-let mkarray n =
-  (* n isn't small, this case is handled separately below *)
-  let lo = n mod base
-  and hi = n / base in
-  let t = if small hi then [|hi;lo|] else [|hi/base;hi mod base;lo|]
-  in
-  for i = Array.length t -1 downto 1 do
-    if t.(i) < 0 then (t.(i) <- t.(i) + base; t.(i-1) <- t.(i-1) -1)
-  done;
-  t
-
-let ints_of_int n =
-  if Int.equal n 0 then [| |]
-  else if small n then [| n |]
-  else mkarray n
-
-let of_int n =
-  if small n then Obj.repr n else Obj.repr (mkarray n)
-
-let of_ints n =
-  let n = normalize n in (* TODO: using normalize here seems redundant now *)
-  if is_zero n then Obj.repr 0 else
-  if Int.equal (Array.length n) 1 then Obj.repr n.(0) else
-  Obj.repr n
-
-let coerce_to_int = (Obj.magic : Obj.t -> int)
-let coerce_to_ints = (Obj.magic : Obj.t -> int array)
-
-let to_ints n =
-  if Obj.is_int n then ints_of_int (coerce_to_int n)
-  else coerce_to_ints n
-
-let int_of_ints =
-  let maxi = mkarray max_int and mini = mkarray min_int in
-  fun t ->
-    let l = Array.length t in
-    if (l > 3) || (Int.equal l 3 && (less_than maxi t || less_than t mini))
-    then failwith "Bigint.to_int: too large";
-    let sum = ref 0 in
-    let pow = ref 1 in
-    for i = l-1 downto 0 do
-      sum := !sum + t.(i) * !pow;
-      pow := !pow*base;
-    done;
-    !sum
-
-let to_int n =
-  if Obj.is_int n then coerce_to_int n
-  else int_of_ints (coerce_to_ints n)
-
-let app_pair f (m, n) =
-  (f m, f n)
-
-let add m n =
-  if Obj.is_int m && Obj.is_int n
-  then of_int (coerce_to_int m + coerce_to_int n)
-  else of_ints (add (to_ints m) (to_ints n))
-
-let sub m n =
-  if Obj.is_int m && Obj.is_int n
-  then of_int (coerce_to_int m - coerce_to_int n)
-  else of_ints (sub (to_ints m) (to_ints n))
-
-let mult m n =
-  if Obj.is_int m && Obj.is_int n
-  then of_int (coerce_to_int m * coerce_to_int n)
-  else of_ints (mult (to_ints m) (to_ints n))
-
-let euclid m n =
-  if Obj.is_int m && Obj.is_int n
-  then app_pair of_int
-    (coerce_to_int m / coerce_to_int n, coerce_to_int m mod coerce_to_int n)
-  else app_pair of_ints (euclid (to_ints m) (to_ints n))
-
-let less_than m n =
-  if Obj.is_int m && Obj.is_int n
-  then coerce_to_int m < coerce_to_int n
-  else less_than (to_ints m) (to_ints n)
-
-let neg n =
-  if Obj.is_int n then of_int (- (coerce_to_int n))
-  else of_ints (neg (to_ints n))
-
-let of_string m = of_ints (of_string m)
-let to_string m = to_string (to_ints m)
-
-let zero = of_int 0
-let one = of_int 1
-let two = of_int 2
-let sub_1 n = sub n one
-let add_1 n = add n one
-let mult_2 n = add n n
-
-let div2_with_rest n =
-  let (q,b) = euclid n two in
-  (q, b == one)
-
-let is_strictly_neg n = is_strictly_neg (to_ints n)
-let is_strictly_pos n = is_strictly_pos (to_ints n)
-let is_neg_or_zero n = is_neg_or_zero (to_ints n)
-let is_pos_or_zero n = is_pos_or_zero (to_ints n)
-
-let equal m n =
-  if Obj.is_block m && Obj.is_block n then
-    ArrayInt.equal (Obj.obj m) (Obj.obj n)
-  else m == n
-
-(* spiwack: computes n^m *)
-(* The basic idea of the algorithm is that n^(2m) = (n^2)^m *)
-(* In practice the algorithm performs :
-    k*n^0 = k
-    k*n^(2m) = k*(n*n)^m
-    k*n^(2m+1) = (n*k)*(n*n)^m *)
-let pow  =
-  let rec pow_aux odd_rest n m = (* odd_rest is the k from above *)
-    if m<=0 then
-      odd_rest
-    else
-      let quo = m lsr 1 (* i.e. m/2 *)
-      and odd = not (Int.equal (m land 1) 0) in
-      pow_aux
-        (if odd then mult n odd_rest else odd_rest)
-        (mult n n)
-        quo
-  in
-  pow_aux one
-
-(** Testing suite w.r.t. OCaml's Big_int *)
-
-(*
-module B = struct
-  open Big_int
-  let zero = zero_big_int
-  let to_string = string_of_big_int
-  let of_string = big_int_of_string
-  let add = add_big_int
-  let opp = minus_big_int
-  let sub = sub_big_int
-  let mul = mult_big_int
-  let abs = abs_big_int
-  let sign = sign_big_int
-  let euclid n m =
-    let n' = abs n and m' = abs m in
-    let q',r' = quomod_big_int n' m' in
-    (if sign (mul n m) < 0 && sign q' <> 0 then opp q' else q'),
-    (if sign n < 0 then opp r' else r')
-end
-
-let check () =
-  let roots = [ 1; 100; base; 100*base; base*base ] in
-  let rands = [ 1234; 5678; 12345678; 987654321 ] in
-  let nums = (List.flatten (List.map (fun x -> [x-1;x;x+1]) roots)) @ rands in
-  let numbers =
-    List.map string_of_int nums @
-    List.map (fun n -> string_of_int (-n)) nums
-  in
-  let i = ref 0 in
-  let compare op x y n n' =
-    incr i;
-    let s = Printf.sprintf "%30s" (to_string n) in
-    let s' = Printf.sprintf "%30s" (B.to_string n') in
-    if s <> s' then Printf.printf "%s%s%s: %s <> %s\n" x op y s s' in
-  let test x y =
-    let n = of_string x and m = of_string y in
-    let n' = B.of_string x and m' = B.of_string y in
-    let a = add n m and a' = B.add n' m' in
-    let s = sub n m and s' = B.sub n' m' in
-    let p = mult n m and p' = B.mul n' m' in
-    let q,r = try euclid n m with Division_by_zero -> zero,zero
-    and q',r' = try B.euclid n' m' with Division_by_zero -> B.zero, B.zero
-    in
-    compare "+" x y a a';
-    compare "-" x y s s';
-    compare "*" x y p p';
-    compare "/" x y q q';
-    compare "%" x y r r'
-  in
-  List.iter (fun a -> List.iter (test a) numbers) numbers;
-  Printf.printf "%i tests done\n" !i
-*)
diff --git a/clib/bigint.mli b/clib/bigint.mli
deleted file mode 100644
index 9677c93873..0000000000
--- a/clib/bigint.mli
+++ /dev/null
@@ -1,53 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(** Arbitrary large integer numbers *)
-
-type bigint
-
-val of_string : string -> bigint
-(** May raise a Failure just as [int_of_string] on non-numerical strings *)
-
-val to_string : bigint -> string
-
-val of_int : int -> bigint
-val to_int : bigint -> int (** May raise a Failure on oversized numbers *)
-
-val zero : bigint
-val one : bigint
-val two : bigint
-
-val div2_with_rest : bigint -> bigint * bool (** true=odd; false=even *)
-
-val add_1 : bigint -> bigint
-val sub_1 : bigint -> bigint
-val mult_2 : bigint -> bigint
-
-val add : bigint -> bigint -> bigint
-val sub : bigint -> bigint -> bigint
-val mult : bigint -> bigint -> bigint
-
-(** Euclid division m/d = (q,r), with m = q*d+r and |r|<|q|.
-    This is the "Trunc" variant (a.k.a "Truncated-Toward-Zero"),
-    as with ocaml's / (but not as ocaml's Big_int.quomod_big_int).
-    We have sign r = sign m *)
-
-val euclid : bigint -> bigint -> bigint * bigint
-
-val less_than : bigint -> bigint -> bool
-val equal : bigint -> bigint -> bool
-
-val is_strictly_pos : bigint -> bool
-val is_strictly_neg : bigint -> bool
-val is_pos_or_zero : bigint -> bool
-val is_neg_or_zero : bigint -> bool
-val neg : bigint -> bigint
-
-val pow : bigint -> int -> bigint
diff --git a/configure.ml b/configure.ml
index 6863d412cc..2d6018491e 100644
--- a/configure.ml
+++ b/configure.ml
@@ -688,19 +688,20 @@ let operating_system =
   else
     (try Sys.getenv "OS" with Not_found -> "")
 
-(** Num library *)
-
-(* since 4.06, the Num library is no longer distributed with OCaml (replaced
-   by Zarith)
-*)
+(** Zarith and num libraries *)
 
 let check_for_numlib () =
   if caml_version_nums >= [4;6;0] then
     let numlib,_ = tryrun camlexec.find ["query";"num"] in
     match numlib with
     | ""  ->
-       die "Num library not installed, required for OCaml 4.06 or later"
-    | _   -> cprintf "You have the Num library installed. Good!"
+      die "Num library not installed, required for OCaml 4.06 or later"
+    | _   -> cprintf "You have the Num library installed. Good!";
+  let zarith,_ = tryrun camlexec.find ["query";"zarith"] in
+  match zarith with
+  | ""  ->
+     die "Zarith library not installed, required"
+  | _   -> cprintf "You have the Zarith library installed. Good!"
 
 let numlib =
   check_for_numlib ()
diff --git a/coq.opam b/coq.opam
index 23cef68dce..f44223052d 100644
--- a/coq.opam
+++ b/coq.opam
@@ -25,6 +25,7 @@ depends: [
   "dune"      { >= "2.5.0"  }
   "ocamlfind" { build }
   "num"
+  "zarith"    { >= "1.9.1" }
 ]
 
 build: [
diff --git a/coq.opam.docker b/coq.opam.docker
index 229a47a87b..ac1869f344 100644
--- a/coq.opam.docker
+++ b/coq.opam.docker
@@ -24,6 +24,7 @@ depends: [
   "ocaml"     { >= "4.05.0" }
   "ocamlfind" { build }
   "num"
+  "zarith"    { >= "1.9.1" }
   "conf-findutils" {build}
 ]
 
diff --git a/default.nix b/default.nix
index df1c43101b..ef969acd31 100644
--- a/default.nix
+++ b/default.nix
@@ -43,7 +43,7 @@ stdenv.mkDerivation rec {
     hostname
     python3 time # coq-makefile timing tools
   ]
-  ++ (with ocamlPackages; [ ocaml findlib ])
+  ++ (with ocamlPackages; [ ocaml findlib num zarith ])
   ++ optionals buildIde [
     ocamlPackages.lablgtk3-sourceview3
     glib gnome3.defaultIconTheme wrapGAppsHook
diff --git a/dev/base_include b/dev/base_include
index 1f14fc2941..daee2d97c5 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -29,7 +29,6 @@
 #install_printer ppatom;;
 #install_printer ppwhd;;
 #install_printer ppvblock;;
-#install_printer  (* bigint *) ppbigint;;
 #install_printer  (* loc *) pploc;;
 #install_printer  (* substitution *) ppsubst;;
 
diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat
index fd6ea9bb09..8eff2cf577 100755
--- a/dev/build/windows/MakeCoq_MinGW.bat
+++ b/dev/build/windows/MakeCoq_MinGW.bat
@@ -389,6 +389,7 @@ IF "%RUNSETUP%"=="Y" (
     -P libfontconfig1 ^

     -P gtk-update-icon-cache ^

     -P libtool,automake ^

+    -P libgmp-devel ^

     -P intltool ^

     -P bison,flex ^

     %EXTRAPACKAGES% ^

diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index cc9fd13fdc..cde1d798a0 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1006,6 +1006,7 @@ function make_ocaml_tools {
 
 function make_ocaml_libs {
   make_num
+  make_zarith
   make_findlib
   make_lablgtk
 }
@@ -1023,6 +1024,16 @@ function make_num {
   fi
 }
 
+function make_zarith {
+  make_ocaml
+  if build_prep https://github.com/ocaml/Zarith/archive release-1.9.1 tar.gz 1 zarith-1.9.1; then
+    logn configure ./configure
+    log1 make
+    log2 make install
+    build_post
+  fi
+}
+
 ##### OCAMLBUILD #####
 
 function make_ocamlbuild {
diff --git a/dev/ci/azure-opam.sh b/dev/ci/azure-opam.sh
index 64936cd236..17d71ac52a 100755
--- a/dev/ci/azure-opam.sh
+++ b/dev/ci/azure-opam.sh
@@ -10,4 +10,4 @@ bash opam64/install.sh
 
 opam init default -a -y "https://github.com/fdopen/opam-repository-mingw.git#opam2" -c $OPAM_VARIANT --disable-sandboxing
 eval "$(opam env)"
-opam install -y num ocamlfind dune ounit
+opam install -y num ocamlfind dune ounit zarith
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 67a8415891..78c8673299 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2020-08-18-V29"
+# CACHEKEY: "bionic_coq-V2020-08-28-V92"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -6,9 +6,14 @@ LABEL maintainer="e@x80.org"
 
 ENV DEBIAN_FRONTEND="noninteractive"
 
+# We need libgmp-dev:i386 for zarith; maybe we could also install GTK
+RUN dpkg --add-architecture i386
+
 RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \
         # Dependencies of the image, the test-suite and external projects
         m4 automake autoconf time wget rsync git gcc-multilib build-essential unzip jq \
+        # Dependencies of ZArith
+        perl libgmp-dev libgmp-dev:i386 \
         # Dependencies of lablgtk (for CoqIDE)
         libgtksourceview-3.0-dev \
         # Dependencies of stdlib and sphinx doc
@@ -35,10 +40,10 @@ ENV NJOBS="2" \
 # Base opam is the set of base packages required by Coq
 ENV COMPILER="4.05.0"
 
-# Common OPAM packages.
-# `num` does not have a version number as the right version to install varies
-# with the compiler version.
-ENV BASE_OPAM="num ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.0" \
+# Common OPAM packages, num to be removed once the migration to
+# micromega is complete, `num` also does not have a version number as
+# the right version to install varies with the compiler version.
+ENV BASE_OPAM="num zarith.1.9.1 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.0" \
     CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \
     BASE_ONLY_OPAM="elpi.1.11.0"
 
@@ -52,9 +57,10 @@ ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.1.0"
 RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam env) && opam update && \
     opam install $BASE_OPAM $COQIDE_OPAM $CI_OPAM $BASE_ONLY_OPAM
 
-# base+32bit switch
+# base+32bit switch, note the zarith hack
 RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
-    opam install $BASE_OPAM
+        i386 env CC='gcc -m32' opam install zarith.1.9.1 && \
+        opam install $BASE_OPAM
 
 # EDGE switch
 ENV COMPILER_EDGE="4.10.0" \
diff --git a/dev/ci/user-overlays/08743-ejgallego-zarith.sh b/dev/ci/user-overlays/08743-ejgallego-zarith.sh
new file mode 100644
index 0000000000..da1d30c1e9
--- /dev/null
+++ b/dev/ci/user-overlays/08743-ejgallego-zarith.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "11742" ] || [ "$CI_BRANCH" = "zarith+core" ]; then
+
+    bignums_CI_REF=zarith
+    bignums_CI_GITURL=https://github.com/ejgallego/bignums
+
+fi
diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg
index 63071bba72..60618f6491 100644
--- a/dev/top_printers.dbg
+++ b/dev/top_printers.dbg
@@ -23,7 +23,6 @@ install_printer Top_printers.ppconstr_expr
 install_printer Top_printers.ppglob_constr
 install_printer Top_printers.pppattern
 install_printer Top_printers.ppfconstr
-install_printer Top_printers.ppbigint
 install_printer Top_printers.ppnumtokunsigned
 install_printer Top_printers.ppnumtokunsignednat
 install_printer Top_printers.ppintset
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index ea90e83a83..773170207e 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -80,7 +80,6 @@ let pppattern = (fun x -> pp(envpp pr_constr_pattern_env x))
 let pptype = (fun x -> try pp(envpp (fun env evm t -> pr_ltype_env env evm t) x) with e -> pp (str (Printexc.to_string e)))
 let ppfconstr c = ppconstr (CClosure.term_of_fconstr c)
 
-let ppbigint n = pp (str (Bigint.to_string n));;
 let ppnumtokunsigned n = pp (NumTok.Unsigned.print n)
 let ppnumtokunsignednat n = pp (NumTok.UnsignedNat.print n)
 
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index 65eab8daa3..b1bb5e4702 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -53,7 +53,6 @@ val ppglob_constr : 'a Glob_term.glob_constr_g -> unit
 val pppattern : Pattern.constr_pattern -> unit
 val ppfconstr : CClosure.fconstr -> unit
 
-val ppbigint : Bigint.bigint -> unit
 val ppnumtokunsigned : NumTok.Unsigned.t -> unit
 val ppnumtokunsignednat : NumTok.UnsignedNat.t -> unit
 
diff --git a/interp/dune b/interp/dune
index e9ef7ba99a..6d73d5724c 100644
--- a/interp/dune
+++ b/interp/dune
@@ -3,4 +3,4 @@
  (synopsis "Coq's Syntactic Interpretation for AST [notations, implicits]")
  (public_name coq.interp)
  (wrapped false)
- (libraries pretyping))
+ (libraries zarith pretyping))
diff --git a/interp/notation.ml b/interp/notation.ml
index 0bd5da5729..c0ebffcdb9 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -388,7 +388,7 @@ module InnerPrimToken = struct
 
   type interpreter =
     | RawNumInterp of (?loc:Loc.t -> rawnum -> glob_constr)
-    | BigNumInterp of (?loc:Loc.t -> Bigint.bigint -> glob_constr)
+    | BigNumInterp of (?loc:Loc.t -> Z.t -> glob_constr)
     | StringInterp of (?loc:Loc.t -> string -> glob_constr)
 
   let interp_eq f f' = match f,f' with
@@ -410,7 +410,7 @@ module InnerPrimToken = struct
 
   type uninterpreter =
     | RawNumUninterp of (any_glob_constr -> rawnum option)
-    | BigNumUninterp of (any_glob_constr -> Bigint.bigint option)
+    | BigNumUninterp of (any_glob_constr -> Z.t option)
     | StringUninterp of (any_glob_constr -> string option)
 
   let uninterp_eq f f' = match f,f' with
@@ -614,11 +614,10 @@ end
 
 (** Conversion from bigint to int63 *)
 let rec int63_of_pos_bigint i =
-  let open Bigint in
-  if equal i zero then Uint63.of_int 0
+  if Z.(equal i zero) then Uint63.of_int 0
   else
-    let (quo,rem) = div2_with_rest i in
-    if rem then Uint63.add (Uint63.of_int 1)
+    let quo, remi = Z.div_rem i (Z.of_int 2) 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)
 
@@ -800,24 +799,24 @@ let rawnum_of_coqint c =
 (** First, [positive] from/to bigint *)
 
 let rec pos_of_bigint posty n =
-  match Bigint.div2_with_rest n with
-  | (q, false) ->
+  match Z.div_rem n (Z.of_int 2) with
+  | (q, rem) when rem = Z.zero ->
       let c = mkConstruct (posty, 2) in (* xO *)
       mkApp (c, [| pos_of_bigint posty q |])
-  | (q, true) when not (Bigint.equal q Bigint.zero) ->
+  | (q, _) when not (Z.equal q Z.zero) ->
       let c = mkConstruct (posty, 1) in (* xI *)
       mkApp (c, [| pos_of_bigint posty q |])
-  | (q, true) ->
+  | (q, _) ->
       mkConstruct (posty, 3) (* xH *)
 
 let rec bigint_of_pos c = match Constr.kind c with
-  | Construct ((_, 3), _) -> (* xH *) Bigint.one
+  | Construct ((_, 3), _) -> (* xH *) Z.one
   | App (c, [| d |]) ->
       begin match Constr.kind c with
       | Construct ((_, n), _) ->
           begin match n with
-          | 1 -> (* xI *) Bigint.add_1 (Bigint.mult_2 (bigint_of_pos d))
-          | 2 -> (* xO *) Bigint.mult_2 (bigint_of_pos d)
+          | 1 -> (* xI *) Z.add Z.one (Z.mul Z.(of_int 2) (bigint_of_pos d))
+          | 2 -> (* xO *) Z.mul Z.(of_int 2) (bigint_of_pos d)
           | n -> assert false (* no other constructor of type positive *)
           end
       | x -> raise NotAValidPrimToken
@@ -827,24 +826,24 @@ let rec bigint_of_pos c = match Constr.kind c with
 (** Now, [Z] from/to bigint *)
 
 let z_of_bigint { z_ty; pos_ty } n =
-  if Bigint.equal n Bigint.zero then
+  if Z.(equal n zero) then
     mkConstruct (z_ty, 1) (* Z0 *)
   else
     let (s, n) =
-      if Bigint.is_pos_or_zero n then (2, n) (* Zpos *)
-      else (3, Bigint.neg n) (* Zneg *)
+      if Z.(leq zero n) then (2, n) (* Zpos *)
+      else (3, Z.neg n) (* Zneg *)
     in
     let c = mkConstruct (z_ty, s) in
     mkApp (c, [| pos_of_bigint pos_ty n |])
 
 let bigint_of_z z = match Constr.kind z with
-  | Construct ((_, 1), _) -> (* Z0 *) Bigint.zero
+  | Construct ((_, 1), _) -> (* Z0 *) Z.zero
   | App (c, [| d |]) ->
       begin match Constr.kind c with
       | Construct ((_, n), _) ->
           begin match n with
           | 2 -> (* Zpos *) bigint_of_pos d
-          | 3 -> (* Zneg *) Bigint.neg (bigint_of_pos d)
+          | 3 -> (* Zneg *) Z.neg (bigint_of_pos d)
           | n -> assert false (* no other constructor of type Z *)
           end
       | _ -> raise NotAValidPrimToken
@@ -861,20 +860,19 @@ let error_negative ?loc =
   CErrors.user_err ?loc ~hdr:"interp_int63" (Pp.str "int63 are only non-negative numbers.")
 
 let error_overflow ?loc n =
-  CErrors.user_err ?loc ~hdr:"interp_int63" Pp.(str "overflow in int63 literal: " ++ str (Bigint.to_string n))
+  CErrors.user_err ?loc ~hdr:"interp_int63" Pp.(str "overflow in int63 literal: " ++ str (Z.to_string n))
 
 let interp_int63 ?loc n =
-  let open Bigint in
-  if is_pos_or_zero n
+  if Z.(leq zero n)
   then
-    if less_than n (pow two 63)
+    if Z.(lt n (pow (of_int 2) 63))
     then int63_of_pos_bigint ?loc n
     else error_overflow ?loc n
   else error_negative ?loc
 
 let bigint_of_int63 c =
   match Constr.kind c with
-  | Int i -> Bigint.of_string (Uint63.to_string i)
+  | Int i -> Z.of_string (Uint63.to_string i)
   | _ -> raise NotAValidPrimToken
 
 let interp o ?loc n =
diff --git a/interp/notation.mli b/interp/notation.mli
index 05ddd25a62..948831b317 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -101,7 +101,7 @@ val register_rawnumeral_interpretation :
   ?allow_overwrite:bool -> prim_token_uid -> rawnum prim_token_interpretation -> unit
 
 val register_bignumeral_interpretation :
-  ?allow_overwrite:bool -> prim_token_uid -> Bigint.bigint prim_token_interpretation -> unit
+  ?allow_overwrite:bool -> prim_token_uid -> Z.t prim_token_interpretation -> unit
 
 val register_string_interpretation :
   ?allow_overwrite:bool -> prim_token_uid -> string prim_token_interpretation -> unit
@@ -196,8 +196,8 @@ val enable_prim_token_interpretation : prim_token_infos -> unit
 *)
 
 val declare_numeral_interpreter : ?local:bool -> scope_name -> required_module ->
-  Bigint.bigint prim_token_interpreter ->
-  glob_constr list * Bigint.bigint prim_token_uninterpreter * bool -> unit
+  Z.t prim_token_interpreter ->
+  glob_constr list * Z.t prim_token_uninterpreter * bool -> unit
 val declare_string_interpreter : ?local:bool -> scope_name -> required_module ->
   string prim_token_interpreter ->
   glob_constr list * string prim_token_uninterpreter * bool -> unit
@@ -349,4 +349,4 @@ val level_of_notation : notation -> level
 val with_notation_protection : ('a -> 'b) -> 'a -> 'b
 
 (** Conversion from bigint to int63 *)
-val int63_of_pos_bigint : Bigint.bigint -> Uint63.t
+val int63_of_pos_bigint : Z.t -> Uint63.t
diff --git a/interp/numTok.ml b/interp/numTok.ml
index bb14649b91..e90e4d25d3 100644
--- a/interp/numTok.ml
+++ b/interp/numTok.ml
@@ -62,6 +62,13 @@ struct
     compare s "0" = 0
 end
 
+(* Helper function *)
+let div2_with_rest =
+  let two = Z.of_int 2 in
+  fun n ->
+    let res, rem = Z.div_rem n two in
+    res, Z.equal rem Z.one
+
 type sign = SPlus | SMinus
 
 type 'a exp = EDec of 'a | EBin of 'a
@@ -84,31 +91,31 @@ struct
     (* nasty code to remove when switching to zarith
        since zarith's of_string handles hexadecimal *)
     match UnsignedNat.classify n with
-    | CDec -> Bigint.of_string (to_string (sign,n))
+    | CDec -> Z.of_string (to_string (sign,n))
     | CHex ->
        let int_of_char c = match c with
          | 'a'..'f' -> 10 + int_of_char c - int_of_char 'a'
          | _ -> int_of_char c - int_of_char '0' in
-       let c16 = Bigint.of_int 16 in
+       let c16 = Z.of_int 16 in
        let s = UnsignedNat.to_string n in
-       let n = ref Bigint.zero in
+       let n = ref Z.zero in
        let len = String.length s in
        for d = 2 to len - 1 do
-         n := Bigint.(add (mult !n c16) (of_int (int_of_char s.[d])))
+         n := Z.(add (mul !n c16) (of_int (int_of_char s.[d])))
        done;
-       match sign with SPlus -> !n | SMinus -> Bigint.neg !n
+       match sign with SPlus -> !n | SMinus -> Z.neg !n
   let to_bigint n = bigint_of_string n
   let string_of_nonneg_bigint c n =
     (* nasty code to remove when switching to zarith
        since zarith's format handles hexadecimal *)
     match c with
-    | CDec -> Bigint.to_string n
+    | CDec -> Z.to_string n
     | CHex ->
        let div16 n =
-         let n, r0 = Bigint.div2_with_rest n in
-         let n, r1 = Bigint.div2_with_rest n in
-         let n, r2 = Bigint.div2_with_rest n in
-         let n, r3 = Bigint.div2_with_rest n in
+         let n, r0 = div2_with_rest n in
+         let n, r1 = div2_with_rest n in
+         let n, r2 = div2_with_rest n in
+         let n, r3 = div2_with_rest n in
          let r = match r3, r2, r1, r0 with
            | false, false, false, false -> "0"
            | false, false, false,  true -> "1"
@@ -129,14 +136,14 @@ struct
          n, r in
        let n = ref n in
        let l = ref [] in
-       while Bigint.is_strictly_pos !n do
+       while Int.equal 1 (Z.sign !n) do
          let n', r = div16 !n in
          n := n';
          l := r :: !l
        done;
        "0x" ^ String.concat "" (List.rev !l)
   let of_bigint c n =
-    let sign, n = if Bigint.is_strictly_neg n then (SMinus, Bigint.neg n) else (SPlus, n) in
+    let sign, n = if Int.equal (-1) (Z.sign n) then (SMinus, Z.neg n) else (SPlus, n) in
     (sign, string_of_nonneg_bigint c n)
 end
 
@@ -339,13 +346,13 @@ struct
     let frac = UnsignedNat.to_string frac in
     let i = SignedNat.to_bigint (s, int ^ frac) in
     let e =
-      let e = if exp = "" then Bigint.zero else match exp.[1] with
-      | '+' -> Bigint.of_string (UnsignedNat.to_string (string_del_head 2 exp))
-      | '-' -> Bigint.(neg (of_string (UnsignedNat.to_string (string_del_head 2 exp))))
-      | _ -> Bigint.of_string (UnsignedNat.to_string (string_del_head 1 exp)) in
+      let e = if exp = "" then Z.zero else match exp.[1] with
+      | '+' -> Z.of_string (UnsignedNat.to_string (string_del_head 2 exp))
+      | '-' -> Z.(neg (of_string (UnsignedNat.to_string (string_del_head 2 exp))))
+      | _ -> Z.of_string (UnsignedNat.to_string (string_del_head 1 exp)) in
       let l = String.length frac in
       let l = match c with CDec -> l | CHex -> 4 * l in
-      Bigint.(sub e (of_int l)) in
+      Z.(sub e (of_int l)) in
     (i, match c with CDec -> EDec e | CHex -> EBin e)
 
   let of_bigint_and_exponent i e =
diff --git a/interp/numTok.mli b/interp/numTok.mli
index 11d5a0f980..bcfe663dd2 100644
--- a/interp/numTok.mli
+++ b/interp/numTok.mli
@@ -65,8 +65,8 @@ sig
 
   val classify : t -> num_class
 
-  val of_bigint : num_class -> Bigint.bigint -> t
-  val to_bigint : t -> Bigint.bigint
+  val of_bigint : num_class -> Z.t -> t
+  val to_bigint : t -> Z.t
 end
 
 (** {6 Unsigned decimal numerals } *)
@@ -131,8 +131,8 @@ sig
   val to_string : t -> string
     (** Returns a string in the syntax of OCaml's float_of_string *)
 
-  val of_bigint : num_class -> Bigint.bigint -> t
-  val to_bigint : t -> Bigint.bigint option
+  val of_bigint : num_class -> Z.t -> t
+  val to_bigint : t -> Z.t option
     (** Convert from and to bigint when the denotation of a bigint *)
 
   val of_int_frac_and_exponent : SignedNat.t -> UnsignedNat.t option -> SignedNat.t option -> t
@@ -140,8 +140,8 @@ sig
     (** n, p and q such that the number is n.p*10^q or n.p*2^q
         pre/postcondition: classify n = classify p, classify q = CDec *)
 
-  val of_bigint_and_exponent : Bigint.bigint -> Bigint.bigint exp -> t
-  val to_bigint_and_exponent : t -> Bigint.bigint * Bigint.bigint exp
+  val of_bigint_and_exponent : Z.t -> Z.t exp -> t
+  val to_bigint_and_exponent : t -> Z.t * Z.t exp
     (** n and p such that the number is n*10^p or n*2^p *)
 
   val classify : t -> num_class
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/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
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 0086516785..02ababd928 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -104,7 +104,7 @@ BEFORE ?=
 AFTER ?=
 
 # FIXME this should be generated by Coq (modules already linked by Coq)
-CAMLDONTLINK=num,str,unix,dynlink,threads
+CAMLDONTLINK=str,unix,dynlink,threads,num,zarith
 
 # OCaml binaries
 CAMLC       ?= "$(OCAMLFIND)" ocamlc   -c
diff --git a/toplevel/dune b/toplevel/dune
index 2d64ae303c..5f10346ac4 100644
--- a/toplevel/dune
+++ b/toplevel/dune
@@ -3,8 +3,9 @@
  (public_name coq.toplevel)
  (synopsis "Coq's Interactive Shell [terminal-based]")
  (wrapped false)
+ ; num still here due to some plugins using it
  (libraries num coq.stm))
-; Coqlevel provides the `Num` library to plugins, we could also use
+; Interp provides the `zarith` library to plugins, we could also use
 ; -linkall in the plugins file, to be discussed.
 
 (coq.pp (modules g_toplevel))