diff --git a/README.md b/README.md
index 61ff1c1..6c06830 100644
--- a/README.md
+++ b/README.md
@@ -52,12 +52,10 @@ With OPAM
 The packages for compilation can also be installed via
 [opam](http://opam.ocaml.org).
 
-    $ opam switch create ocaml-base-compiler.4.08.1
+    $ opam switch create 5.3.0
     $ eval $(opam env)
     $ opam repo add coq-released https://coq.inria.fr/opam/released
     $ opam install dune zarith lwt lwt_ppx
-    $ opam pin coq 8.11.0
-    $ opam pin coq-mathcomp-ssreflect 1.10.0
     $ opam install coq-mathcomp-algebra
 
 Some system dependencies such as libgmp-dev on Ubuntu 20.04 may need to be
diff --git a/src/ocaml/extraction/Ascii.ml b/src/ocaml/extraction/Ascii.ml
index d4175db..4d474d3 100644
--- a/src/ocaml/extraction/Ascii.ml
+++ b/src/ocaml/extraction/Ascii.ml
@@ -24,8 +24,8 @@ let ascii_of_pos =
       | Coq_xO p' -> shift false (loop n' p')
       | Coq_xH -> one)
       n
-  in loop (Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-       (Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
+  in loop (Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+       (Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
        0))))))))
 
 (** val ascii_of_N : coq_N -> char **)
diff --git a/src/ocaml/extraction/BBAshr.ml b/src/ocaml/extraction/BBAshr.ml
index 6e1fbb4..f58ab87 100644
--- a/src/ocaml/extraction/BBAshr.ml
+++ b/src/ocaml/extraction/BBAshr.ml
@@ -60,7 +60,7 @@ let rec bit_blast_ashr_rec g ls ns i =
     generator -> literal list -> literal list -> (generator * cnf) * word **)
 
 let bit_blast_ashr g ls ns =
-  if leq (Pervasives.succ (Pervasives.succ 0)) (size ls)
+  if leq (Stdlib.succ (Stdlib.succ 0)) (size ls)
   then let (p, zero_hi) =
          bit_blast_const g
            (from_nat
diff --git a/src/ocaml/extraction/BBExtract.ml b/src/ocaml/extraction/BBExtract.ml
index 1889c87..4b30d0e 100644
--- a/src/ocaml/extraction/BBExtract.ml
+++ b/src/ocaml/extraction/BBExtract.ml
@@ -8,10 +8,10 @@ open Ssrnat
 
 let bit_blast_extract g i j ls =
   let lowls =
-    cat (take (addn i (Pervasives.succ 0)) ls)
-      (nseq (subn (addn i (Pervasives.succ 0)) (size ls)) lit_ff)
+    cat (take (addn i (Stdlib.succ 0)) ls)
+      (nseq (subn (addn i (Stdlib.succ 0)) (size ls)) lit_ff)
   in
   ((g, []),
   (cat
-    (nseq (subn (addn (subn i j) (Pervasives.succ 0)) (size lowls)) lit_ff)
-    (drop (subn (size lowls) (addn (subn i j) (Pervasives.succ 0))) lowls)))
+    (nseq (subn (addn (subn i j) (Stdlib.succ 0)) (size lowls)) lit_ff)
+    (drop (subn (size lowls) (addn (subn i j) (Stdlib.succ 0))) lowls)))
diff --git a/src/ocaml/extraction/BBLshr.ml b/src/ocaml/extraction/BBLshr.ml
index 829f9f1..163e061 100644
--- a/src/ocaml/extraction/BBLshr.ml
+++ b/src/ocaml/extraction/BBLshr.ml
@@ -59,7 +59,7 @@ let rec bit_blast_lshr_rec g ls ns i =
     generator -> literal list -> literal list -> (generator * cnf) * word **)
 
 let bit_blast_lshr g ls ns =
-  if leq (Pervasives.succ (Pervasives.succ 0)) (size ls)
+  if leq (Stdlib.succ (Stdlib.succ 0)) (size ls)
   then let (p, zero_hi) =
          bit_blast_const g
            (from_nat
diff --git a/src/ocaml/extraction/BBNeg.ml b/src/ocaml/extraction/BBNeg.ml
index 0665650..fe21b48 100644
--- a/src/ocaml/extraction/BBNeg.ml
+++ b/src/ocaml/extraction/BBNeg.ml
@@ -13,7 +13,7 @@ let bit_blast_neg g ls =
   let (p, lrs_not) = bit_blast_not g ls in
   let (g_not, cs_not) = p in
   let (p0, lrs_con) =
-    bit_blast_const g_not (from_nat (size ls) (Pervasives.succ 0))
+    bit_blast_const g_not (from_nat (size ls) (Stdlib.succ 0))
   in
   let (g_con, cs_con) = p0 in
   let (p1, lrs_add) = bit_blast_add g_con lrs_not lrs_con in
diff --git a/src/ocaml/extraction/BBShl.ml b/src/ocaml/extraction/BBShl.ml
index 3eeff30..87ec30f 100644
--- a/src/ocaml/extraction/BBShl.ml
+++ b/src/ocaml/extraction/BBShl.ml
@@ -59,7 +59,7 @@ let rec bit_blast_shl_rec g ls ns i =
     generator -> literal list -> literal list -> (generator * cnf) * word **)
 
 let bit_blast_shl g ls ns =
-  if leq (Pervasives.succ (Pervasives.succ 0)) (size ls)
+  if leq (Stdlib.succ (Stdlib.succ 0)) (size ls)
   then let (p, zero_hi) =
          bit_blast_const g
            (from_nat
diff --git a/src/ocaml/extraction/BBSmulo.ml b/src/ocaml/extraction/BBSmulo.ml
index 73c6a5d..e419ab7 100644
--- a/src/ocaml/extraction/BBSmulo.ml
+++ b/src/ocaml/extraction/BBSmulo.ml
@@ -35,9 +35,9 @@ let bit_blast_smulo g ls1 ls2 =
   in
   let (p2, _) = p1 in
   let (g_rec, cs_rec) = p2 in
-  let (p3, wls1) = bit_blast_signextend (Pervasives.succ 0) g_rec ls1 in
+  let (p3, wls1) = bit_blast_signextend (Stdlib.succ 0) g_rec ls1 in
   let (g_wls1, cs_wls1) = p3 in
-  let (p4, wls2) = bit_blast_signextend (Pervasives.succ 0) g_wls1 ls2 in
+  let (p4, wls2) = bit_blast_signextend (Stdlib.succ 0) g_wls1 ls2 in
   let (g_wls2, cs_wls2) = p4 in
   let (p5, mul) = bit_blast_mul g_wls2 wls1 (Obj.magic wls2) in
   let (g_mul, cs_mul) = p5 in
diff --git a/src/ocaml/extraction/BBUmulo.ml b/src/ocaml/extraction/BBUmulo.ml
index 4b2cab9..d843e4f 100644
--- a/src/ocaml/extraction/BBUmulo.ml
+++ b/src/ocaml/extraction/BBUmulo.ml
@@ -43,9 +43,9 @@ let bit_blast_umulo_rec g ls1 ls2 =
 let bit_blast_umulo g ls1 ls2 =
   let ls1_hightl = snd (splitlsl ls1) in
   let ls2_hightl = snd (splitlsl ls2) in
-  let (p, lrs_wls1) = bit_blast_zeroextend (Pervasives.succ 0) g ls1 in
+  let (p, lrs_wls1) = bit_blast_zeroextend (Stdlib.succ 0) g ls1 in
   let (g_wls1, cs_wls1) = p in
-  let (p0, lrs_wls2) = bit_blast_zeroextend (Pervasives.succ 0) g_wls1 ls2 in
+  let (p0, lrs_wls2) = bit_blast_zeroextend (Stdlib.succ 0) g_wls1 ls2 in
   let (g_wls2, cs_wls2) = p0 in
   let (p1, r_or_and_rec1) = bit_blast_umulo_rec g_wls2 ls1_hightl ls2_hightl
   in
diff --git a/src/ocaml/extraction/BinPos.ml b/src/ocaml/extraction/BinPos.ml
index 5a862bd..b499093 100644
--- a/src/ocaml/extraction/BinPos.ml
+++ b/src/ocaml/extraction/BinPos.ml
@@ -231,7 +231,7 @@ module Pos =
   (** val to_nat : positive -> int **)
 
   let to_nat x =
-    iter_op Nat0.add x (Pervasives.succ 0)
+    iter_op Nat0.add x (Stdlib.succ 0)
 
   (** val of_nat : int -> positive **)
 
diff --git a/src/ocaml/extraction/DSL.ml b/src/ocaml/extraction/DSL.ml
index 77703e9..f87a9d3 100644
--- a/src/ocaml/extraction/DSL.ml
+++ b/src/ocaml/extraction/DSL.ml
@@ -2022,25 +2022,25 @@ module MakeDSL =
   (** val well_typed_rexp : TE.env -> rexp -> bool **)
 
   let rec well_typed_rexp te = function
-  | Rvar v -> leq (Pervasives.succ 0) (TE.vsize v te)
+  | Rvar v -> leq (Stdlib.succ 0) (TE.vsize v te)
   | Rconst (w, n) ->
-    (&&) (leq (Pervasives.succ 0) w)
+    (&&) (leq (Stdlib.succ 0) w)
       (eq_op nat_eqType (Obj.magic size n) (Obj.magic w))
   | Runop (w, _, e0) ->
-    (&&) ((&&) (leq (Pervasives.succ 0) w) (well_typed_rexp te e0))
+    (&&) ((&&) (leq (Stdlib.succ 0) w) (well_typed_rexp te e0))
       (eq_op nat_eqType (Obj.magic size_of_rexp e0 te) (Obj.magic w))
   | Rbinop (w, _, e1, e2) ->
     (&&)
       ((&&)
-        ((&&) ((&&) (leq (Pervasives.succ 0) w) (well_typed_rexp te e1))
+        ((&&) ((&&) (leq (Stdlib.succ 0) w) (well_typed_rexp te e1))
           (eq_op nat_eqType (Obj.magic size_of_rexp e1 te) (Obj.magic w)))
         (well_typed_rexp te e2))
       (eq_op nat_eqType (Obj.magic size_of_rexp e2 te) (Obj.magic w))
   | Ruext (w, e0, _) ->
-    (&&) ((&&) (leq (Pervasives.succ 0) w) (well_typed_rexp te e0))
+    (&&) ((&&) (leq (Stdlib.succ 0) w) (well_typed_rexp te e0))
       (eq_op nat_eqType (Obj.magic size_of_rexp e0 te) (Obj.magic w))
   | Rsext (w, e0, _) ->
-    (&&) ((&&) (leq (Pervasives.succ 0) w) (well_typed_rexp te e0))
+    (&&) ((&&) (leq (Stdlib.succ 0) w) (well_typed_rexp te e0))
       (eq_op nat_eqType (Obj.magic size_of_rexp e0 te) (Obj.magic w))
 
   (** val well_typed_ebexp : TE.env -> ebexp -> bool **)
@@ -2060,14 +2060,14 @@ module MakeDSL =
   | Req (w, e1, e2) ->
     (&&)
       ((&&)
-        ((&&) ((&&) (leq (Pervasives.succ 0) w) (well_typed_rexp te e1))
+        ((&&) ((&&) (leq (Stdlib.succ 0) w) (well_typed_rexp te e1))
           (eq_op nat_eqType (Obj.magic size_of_rexp e1 te) (Obj.magic w)))
         (well_typed_rexp te e2))
       (eq_op nat_eqType (Obj.magic size_of_rexp e2 te) (Obj.magic w))
   | Rcmp (w, _, e1, e2) ->
     (&&)
       ((&&)
-        ((&&) ((&&) (leq (Pervasives.succ 0) w) (well_typed_rexp te e1))
+        ((&&) ((&&) (leq (Stdlib.succ 0) w) (well_typed_rexp te e1))
           (eq_op nat_eqType (Obj.magic size_of_rexp e1 te) (Obj.magic w)))
         (well_typed_rexp te e2))
       (eq_op nat_eqType (Obj.magic size_of_rexp e2 te) (Obj.magic w))
@@ -2084,8 +2084,8 @@ module MakeDSL =
 
   let well_sized_atom e a =
     if is_unsigned (atyp a e)
-    then leq (Pervasives.succ 0) (asize a e)
-    else leq (Pervasives.succ (Pervasives.succ 0)) (asize a e)
+    then leq (Stdlib.succ 0) (asize a e)
+    else leq (Stdlib.succ (Stdlib.succ 0)) (asize a e)
 
   (** val size_matched_atom : atom -> bool **)
 
@@ -2104,7 +2104,7 @@ module MakeDSL =
   let well_typed_instr e = function
   | Imov (_, a) -> well_typed_atom e a
   | Ishl (_, a, n) ->
-    (&&) (well_typed_atom e a) (leq (Pervasives.succ n) (asize a e))
+    (&&) (well_typed_atom e a) (leq (Stdlib.succ n) (asize a e))
   | Icshl (_, _, a1, a2, n) ->
     (&&)
       ((&&)
@@ -2208,7 +2208,7 @@ module MakeDSL =
       ((&&) (eq_op typ_eqType (Obj.magic atyp a1 e) (Obj.magic atyp a2 e))
         (well_typed_atom e a1)) (well_typed_atom e a2)
   | Isplit (_, _, a, n) ->
-    (&&) (well_typed_atom e a) (leq (Pervasives.succ n) (asize a e))
+    (&&) (well_typed_atom e a) (leq (Stdlib.succ n) (asize a e))
   | Iand (_, t0, a1, a2) ->
     (&&)
       ((&&) ((&&) (compatible t0 (atyp a1 e)) (compatible t0 (atyp a2 e)))
diff --git a/src/ocaml/extraction/DSLLite.ml b/src/ocaml/extraction/DSLLite.ml
index 3e15e14..365f9b4 100644
--- a/src/ocaml/extraction/DSLLite.ml
+++ b/src/ocaml/extraction/DSLLite.ml
@@ -2106,25 +2106,25 @@ module MakeDSL =
   (** val well_typed_rexp : TE.env -> rexp -> bool **)
 
   let rec well_typed_rexp te = function
-  | Rvar v -> leq (Pervasives.succ 0) (TE.vsize v te)
+  | Rvar v -> leq (Stdlib.succ 0) (TE.vsize v te)
   | Rconst (w, n) ->
-    (&&) (leq (Pervasives.succ 0) w)
+    (&&) (leq (Stdlib.succ 0) w)
       (eq_op nat_eqType (Obj.magic size n) (Obj.magic w))
   | Runop (w, _, e0) ->
-    (&&) ((&&) (leq (Pervasives.succ 0) w) (well_typed_rexp te e0))
+    (&&) ((&&) (leq (Stdlib.succ 0) w) (well_typed_rexp te e0))
       (eq_op nat_eqType (Obj.magic size_of_rexp e0 te) (Obj.magic w))
   | Rbinop (w, _, e1, e2) ->
     (&&)
       ((&&)
-        ((&&) ((&&) (leq (Pervasives.succ 0) w) (well_typed_rexp te e1))
+        ((&&) ((&&) (leq (Stdlib.succ 0) w) (well_typed_rexp te e1))
           (eq_op nat_eqType (Obj.magic size_of_rexp e1 te) (Obj.magic w)))
         (well_typed_rexp te e2))
       (eq_op nat_eqType (Obj.magic size_of_rexp e2 te) (Obj.magic w))
   | Ruext (w, e0, _) ->
-    (&&) ((&&) (leq (Pervasives.succ 0) w) (well_typed_rexp te e0))
+    (&&) ((&&) (leq (Stdlib.succ 0) w) (well_typed_rexp te e0))
       (eq_op nat_eqType (Obj.magic size_of_rexp e0 te) (Obj.magic w))
   | Rsext (w, e0, _) ->
-    (&&) ((&&) (leq (Pervasives.succ 0) w) (well_typed_rexp te e0))
+    (&&) ((&&) (leq (Stdlib.succ 0) w) (well_typed_rexp te e0))
       (eq_op nat_eqType (Obj.magic size_of_rexp e0 te) (Obj.magic w))
 
   (** val well_typed_ebexp : TE.env -> ebexp -> bool **)
@@ -2144,14 +2144,14 @@ module MakeDSL =
   | Req (w, e1, e2) ->
     (&&)
       ((&&)
-        ((&&) ((&&) (leq (Pervasives.succ 0) w) (well_typed_rexp te e1))
+        ((&&) ((&&) (leq (Stdlib.succ 0) w) (well_typed_rexp te e1))
           (eq_op nat_eqType (Obj.magic size_of_rexp e1 te) (Obj.magic w)))
         (well_typed_rexp te e2))
       (eq_op nat_eqType (Obj.magic size_of_rexp e2 te) (Obj.magic w))
   | Rcmp (w, _, e1, e2) ->
     (&&)
       ((&&)
-        ((&&) ((&&) (leq (Pervasives.succ 0) w) (well_typed_rexp te e1))
+        ((&&) ((&&) (leq (Stdlib.succ 0) w) (well_typed_rexp te e1))
           (eq_op nat_eqType (Obj.magic size_of_rexp e1 te) (Obj.magic w)))
         (well_typed_rexp te e2))
       (eq_op nat_eqType (Obj.magic size_of_rexp e2 te) (Obj.magic w))
@@ -2168,8 +2168,8 @@ module MakeDSL =
 
   let well_sized_atom e a =
     if is_unsigned (atyp a e)
-    then leq (Pervasives.succ 0) (asize a e)
-    else leq (Pervasives.succ (Pervasives.succ 0)) (asize a e)
+    then leq (Stdlib.succ 0) (asize a e)
+    else leq (Stdlib.succ (Stdlib.succ 0)) (asize a e)
 
   (** val size_matched_atom : atom -> bool **)
 
@@ -2188,7 +2188,7 @@ module MakeDSL =
   let well_typed_instr e = function
   | Imov (_, a) -> well_typed_atom e a
   | Ishl (_, a, n) ->
-    (&&) (well_typed_atom e a) (leq (Pervasives.succ n) (asize a e))
+    (&&) (well_typed_atom e a) (leq (Stdlib.succ n) (asize a e))
   | Icshl (_, _, a1, a2, n) ->
     (&&)
       ((&&)
@@ -2292,7 +2292,7 @@ module MakeDSL =
       ((&&) (eq_op typ_eqType (Obj.magic atyp a1 e) (Obj.magic atyp a2 e))
         (well_typed_atom e a1)) (well_typed_atom e a2)
   | Isplit (_, _, a, n) ->
-    (&&) (well_typed_atom e a) (leq (Pervasives.succ n) (asize a e))
+    (&&) (well_typed_atom e a) (leq (Stdlib.succ n) (asize a e))
   | Iand (_, t0, a1, a2) ->
     (&&)
       ((&&) ((&&) (compatible t0 (atyp a1 e)) (compatible t0 (atyp a2 e)))
@@ -2663,7 +2663,7 @@ module MakeDSL =
       options -> ebexp -> program -> (VS.t -> VS.t) -> VS.t -> VS.t **)
 
   let depvars_epre_eprogram_sat_F o e p depvars_epre_eprogram_sat0 vs =
-    if leq (Pervasives.succ (VS.cardinal vs))
+    if leq (Stdlib.succ (VS.cardinal vs))
          (VS.cardinal (depvars_epre_eprogram o vs e p))
     then depvars_epre_eprogram_sat0 (depvars_epre_eprogram o vs e p)
     else depvars_epre_eprogram o vs e p
@@ -2672,7 +2672,7 @@ module MakeDSL =
       options -> ebexp -> program -> VS.t -> VS.t **)
 
   let rec depvars_epre_eprogram_sat_terminate o e p vs =
-    if leq (Pervasives.succ (VS.cardinal vs))
+    if leq (Stdlib.succ (VS.cardinal vs))
          (VS.cardinal (depvars_epre_eprogram o vs e p))
     then depvars_epre_eprogram_sat_terminate o e p
            (depvars_epre_eprogram o vs e p)
@@ -2718,7 +2718,7 @@ module MakeDSL =
   let rec depvars_epre_eprogram_sat_rect o e p f f0 vs =
     let f1 = f0 vs in
     let f2 = f vs in
-    if leq (Pervasives.succ (VS.cardinal vs))
+    if leq (Stdlib.succ (VS.cardinal vs))
          (VS.cardinal (depvars_epre_eprogram o vs e p))
     then let f3 = f2 __ in
          let hrec =
@@ -2750,7 +2750,7 @@ module MakeDSL =
       options -> rbexp -> program -> (VS.t -> VS.t) -> VS.t -> VS.t **)
 
   let depvars_rpre_rprogram_sat_F o r p depvars_rpre_rprogram_sat0 vs =
-    if leq (Pervasives.succ (VS.cardinal vs))
+    if leq (Stdlib.succ (VS.cardinal vs))
          (VS.cardinal (depvars_rpre_rprogram o vs r p))
     then depvars_rpre_rprogram_sat0 (depvars_rpre_rprogram o vs r p)
     else depvars_rpre_rprogram o vs r p
@@ -2759,7 +2759,7 @@ module MakeDSL =
       options -> rbexp -> program -> VS.t -> VS.t **)
 
   let rec depvars_rpre_rprogram_sat_terminate o r p vs =
-    if leq (Pervasives.succ (VS.cardinal vs))
+    if leq (Stdlib.succ (VS.cardinal vs))
          (VS.cardinal (depvars_rpre_rprogram o vs r p))
     then depvars_rpre_rprogram_sat_terminate o r p
            (depvars_rpre_rprogram o vs r p)
@@ -2805,7 +2805,7 @@ module MakeDSL =
   let rec depvars_rpre_rprogram_sat_rect o r p f f0 vs =
     let f1 = f0 vs in
     let f2 = f vs in
-    if leq (Pervasives.succ (VS.cardinal vs))
+    if leq (Stdlib.succ (VS.cardinal vs))
          (VS.cardinal (depvars_rpre_rprogram o vs r p))
     then let f3 = f2 __ in
          let hrec =
diff --git a/src/ocaml/extraction/DSLRaw.ml b/src/ocaml/extraction/DSLRaw.ml
index 04beda8..c6b1993 100644
--- a/src/ocaml/extraction/DSLRaw.ml
+++ b/src/ocaml/extraction/DSLRaw.ml
@@ -376,7 +376,7 @@ let rec limbsi var i r = function
    | [] -> e
    | _ :: _ ->
      eadd var (emul var e (e2expn var (Z.mul (Z.of_nat i) r)))
-       (limbsi var (addn i (Pervasives.succ 0)) r es0))
+       (limbsi var (addn i (Stdlib.succ 0)) r es0))
 
 type rexp =
 | Rvar of Equality.sort
@@ -413,7 +413,7 @@ let radds var w = function
 (** val rmuls : Equality.coq_type -> int -> rexp list -> rexp **)
 
 let rmuls var w = function
-| [] -> rbits var (from_nat w (Pervasives.succ 0))
+| [] -> rbits var (from_nat w (Stdlib.succ 0))
 | e :: es0 ->
   (match es0 with
    | [] -> e
diff --git a/src/ocaml/extraction/EqFMaps.ml b/src/ocaml/extraction/EqFMaps.ml
index 39c27b3..c250542 100644
--- a/src/ocaml/extraction/EqFMaps.ml
+++ b/src/ocaml/extraction/EqFMaps.ml
@@ -264,7 +264,7 @@ module MakeTreeMap' =
 
     let rec cardinal = function
     | Leaf -> 0
-    | Node (l, _, _, r, _) -> Pervasives.succ (add (cardinal l) (cardinal r))
+    | Node (l, _, _, r, _) -> Stdlib.succ (add (cardinal l) (cardinal r))
 
     (** val empty : 'a1 tree **)
 
diff --git a/src/ocaml/extraction/External.ml b/src/ocaml/extraction/External.ml
index c52042b..b97f544 100644
--- a/src/ocaml/extraction/External.ml
+++ b/src/ocaml/extraction/External.ml
@@ -722,7 +722,7 @@ let rec coq_magma_of_pexpr e =
 
 module PosOrder = struct
   type t = positive
-  let compare = Pervasives.compare
+  let compare = Stdlib.compare
 end
 
 module PS = Set.Make(PosOrder)
diff --git a/src/ocaml/extraction/ExtrOcamlIntConv.ml b/src/ocaml/extraction/ExtrOcamlIntConv.ml
index 552f712..46829aa 100644
--- a/src/ocaml/extraction/ExtrOcamlIntConv.ml
+++ b/src/ocaml/extraction/ExtrOcamlIntConv.ml
@@ -32,7 +32,7 @@ let int_natlike_rec = fun fO fS ->
 (** val nat_of_int : int -> int **)
 
 let nat_of_int =
-  int_natlike_rec 0 (fun x -> Pervasives.succ x)
+  int_natlike_rec 0 (fun x -> Stdlib.succ x)
 
 (** val int_poslike_rec :
     'a1 -> ('a1 -> 'a1) -> ('a1 -> 'a1) -> int -> 'a1 **)
diff --git a/src/ocaml/extraction/IMP.ml b/src/ocaml/extraction/IMP.ml
index 1ff703e..258812b 100644
--- a/src/ocaml/extraction/IMP.ml
+++ b/src/ocaml/extraction/IMP.ml
@@ -206,7 +206,7 @@ let rec pexpr_single_variables = function
 let rec pexpr_num_occurrence v = function
 | PEX j ->
   if eq_op pos_eqType (Obj.magic j) (Obj.magic v)
-  then Pervasives.succ 0
+  then Stdlib.succ 0
   else 0
 | PEadd (e1, e2) ->
   addn (pexpr_num_occurrence v e1) (pexpr_num_occurrence v e2)
@@ -250,7 +250,7 @@ let pexpr_get_rewrite_pattern e =
   let candidates =
     PS.filter (fun v ->
       eq_op nat_eqType (Obj.magic pexpr_num_occurrence v e)
-        (Obj.magic (Pervasives.succ 0))) (pexpr_single_variables e)
+        (Obj.magic (Stdlib.succ 0))) (pexpr_single_variables e)
   in
   if eq_op nat_eqType (Obj.magic PS.cardinal candidates) (Obj.magic 0)
   then None
diff --git a/src/ocaml/extraction/MSetAVL.ml b/src/ocaml/extraction/MSetAVL.ml
index 215aa6c..916a1c8 100644
--- a/src/ocaml/extraction/MSetAVL.ml
+++ b/src/ocaml/extraction/MSetAVL.ml
@@ -92,21 +92,21 @@ module MakeRaw =
 
   let rec cardinal = function
   | Leaf -> 0
-  | Node (_, l, _, r) -> Pervasives.succ (add (cardinal l) (cardinal r))
+  | Node (_, l, _, r) -> Stdlib.succ (add (cardinal l) (cardinal r))
 
   (** val maxdepth : tree -> int **)
 
   let rec maxdepth = function
   | Leaf -> 0
   | Node (_, l, _, r) ->
-    Pervasives.succ (Pervasives.max (maxdepth l) (maxdepth r))
+    Stdlib.succ (Stdlib.max (maxdepth l) (maxdepth r))
 
   (** val mindepth : tree -> int **)
 
   let rec mindepth = function
   | Leaf -> 0
   | Node (_, l, _, r) ->
-    Pervasives.succ (Pervasives.min (mindepth l) (mindepth r))
+    Stdlib.succ (Stdlib.min (mindepth l) (mindepth r))
 
   (** val for_all : (elt -> bool) -> tree -> bool **)
 
diff --git a/src/ocaml/extraction/NBitsDef.ml b/src/ocaml/extraction/NBitsDef.ml
index e446547..53ba14c 100644
--- a/src/ocaml/extraction/NBitsDef.ml
+++ b/src/ocaml/extraction/NBitsDef.ml
@@ -103,8 +103,8 @@ let low n bs =
 (** val extract : int -> int -> bits -> bits **)
 
 let extract i j bs =
-  high (addn (subn i j) (Pervasives.succ 0))
-    (low (addn i (Pervasives.succ 0)) bs)
+  high (addn (subn i j) (Stdlib.succ 0))
+    (low (addn i (Stdlib.succ 0)) bs)
 
 (** val zext : int -> bits -> bits **)
 
@@ -213,16 +213,16 @@ let rec to_hex bs = match bs with
    | [] ->
      append_nibble_on_string
        (cat bs
-         (zeros (Pervasives.succ (Pervasives.succ (Pervasives.succ 0))))) []
+         (zeros (Stdlib.succ (Stdlib.succ (Stdlib.succ 0))))) []
    | b3 :: l0 ->
      (match l0 with
       | [] ->
         append_nibble_on_string
-          (cat bs (zeros (Pervasives.succ (Pervasives.succ 0)))) []
+          (cat bs (zeros (Stdlib.succ (Stdlib.succ 0)))) []
       | b4 :: l1 ->
         (match l1 with
          | [] ->
-           append_nibble_on_string (cat bs (zeros (Pervasives.succ 0))) []
+           append_nibble_on_string (cat bs (zeros (Stdlib.succ 0))) []
          | b5 :: tl ->
            append_nibble_on_string (b2 :: (b3 :: (b4 :: (b5 :: []))))
              (to_hex tl))))
diff --git a/src/ocaml/extraction/NBitsOp.ml b/src/ocaml/extraction/NBitsOp.ml
index 0da17df..850a0d8 100644
--- a/src/ocaml/extraction/NBitsOp.ml
+++ b/src/ocaml/extraction/NBitsOp.ml
@@ -182,8 +182,8 @@ let mulB bs1 bs2 =
 let coq_Umulo bs1 bs2 =
   let bs1_hightl = snd (splitlsb bs1) in
   let bs2_hightl = snd (splitlsb bs2) in
-  let wbs1 = zext (Pervasives.succ 0) bs1 in
-  let wbs2 = zext (Pervasives.succ 0) bs2 in
+  let wbs1 = zext (Stdlib.succ 0) bs1 in
+  let wbs2 = zext (Stdlib.succ 0) bs2 in
   let mul = mulB wbs1 wbs2 in
   let mul_high = msb mul in (||) (andb_orb_all bs1_hightl bs2_hightl) mul_high
 
@@ -201,8 +201,8 @@ let coq_Smulo bs1 bs2 =
   let xbs1_hightl = snd (splitlsb xbs1) in
   let xbs2_hightl = snd (splitlsb xbs2) in
   let and_or = andb_orb_all xbs1_hightl xbs2_hightl in
-  let wbs1 = sext (Pervasives.succ 0) bs1 in
-  let wbs2 = sext (Pervasives.succ 0) bs2 in
+  let wbs1 = sext (Stdlib.succ 0) bs1 in
+  let wbs2 = sext (Stdlib.succ 0) bs2 in
   let mul = mulB wbs1 wbs2 in
   let mul_tl = fst (splitmsb mul) in
   let mul_n = snd (splitmsb mul) in
@@ -303,7 +303,7 @@ let shrBB bs ns =
   let szbs = size bs in
   let szns = size ns in
   let log2szbs = Nat.log2_up szbs in
-  if leq szbs (Pervasives.succ 0)
+  if leq szbs (Stdlib.succ 0)
   then if eq_op bitseq_eqType (Obj.magic ns) (Obj.magic zeros szns)
        then bs
        else zeros szbs
@@ -332,7 +332,7 @@ let sarBB bs ns =
   let szns = size ns in
   let log2szbs = Nat.log2_up szbs in
   let msb_bs = msb bs in
-  if leq szbs (Pervasives.succ 0)
+  if leq szbs (Stdlib.succ 0)
   then if eq_op bitseq_eqType (Obj.magic ns) (Obj.magic zeros szns)
        then bs
        else nseq szbs msb_bs
@@ -360,7 +360,7 @@ let shlBB bs ns =
   let szbs = size bs in
   let szns = size ns in
   let log2szbs = Nat.log2_up szbs in
-  if leq szbs (Pervasives.succ 0)
+  if leq szbs (Stdlib.succ 0)
   then if eq_op bitseq_eqType (Obj.magic ns) (Obj.magic zeros szns)
        then bs
        else zeros szbs
diff --git a/src/ocaml/extraction/Nat0.ml b/src/ocaml/extraction/Nat0.ml
index e2344c1..18f0713 100644
--- a/src/ocaml/extraction/Nat0.ml
+++ b/src/ocaml/extraction/Nat0.ml
@@ -1,7 +1,7 @@
 
 (** val pred : int -> int **)
 
-let pred = fun n -> Pervasives.max 0 (n-1)
+let pred = fun n -> Stdlib.max 0 (n-1)
 
 (** val add : int -> int -> int **)
 
@@ -13,6 +13,6 @@ let rec mul = ( * )
 
 (** val sub : int -> int -> int **)
 
-let rec sub = fun n m -> Pervasives.max 0 (n-m)
+let rec sub = fun n m -> Stdlib.max 0 (n-m)
 
 
diff --git a/src/ocaml/extraction/PeanoNat.ml b/src/ocaml/extraction/PeanoNat.ml
index 5bab96b..27b5f9e 100644
--- a/src/ocaml/extraction/PeanoNat.ml
+++ b/src/ocaml/extraction/PeanoNat.ml
@@ -36,20 +36,20 @@ module Nat =
       (fun k' ->
       (fun fO fS n -> if n=0 then fO () else fS (n-1))
         (fun _ ->
-        log2_iter k' (Pervasives.succ p) (Pervasives.succ q) q)
-        (fun r' -> log2_iter k' p (Pervasives.succ q) r')
+        log2_iter k' (Stdlib.succ p) (Stdlib.succ q) q)
+        (fun r' -> log2_iter k' p (Stdlib.succ q) r')
         r)
       k
 
   (** val log2 : int -> int **)
 
   let log2 n =
-    log2_iter (pred n) 0 (Pervasives.succ 0) 0
+    log2_iter (pred n) 0 (Stdlib.succ 0) 0
 
   (** val log2_up : int -> int **)
 
   let log2_up a =
-    match compare (Pervasives.succ 0) a with
-    | Lt -> Pervasives.succ (log2 (pred a))
+    match compare (Stdlib.succ 0) a with
+    | Lt -> Stdlib.succ (log2 (pred a))
     | _ -> 0
  end
diff --git a/src/ocaml/extraction/QFBV.ml b/src/ocaml/extraction/QFBV.ml
index 45aa2ae..98b57cf 100644
--- a/src/ocaml/extraction/QFBV.ml
+++ b/src/ocaml/extraction/QFBV.ml
@@ -988,7 +988,7 @@ module MakeQFBV =
   (** val qfbv_one : int -> exp **)
 
   let qfbv_one w =
-    Econst (from_nat w (Pervasives.succ 0))
+    Econst (from_nat w (Stdlib.succ 0))
 
   (** val qfbv_not : exp -> exp **)
 
@@ -1297,31 +1297,31 @@ module MakeQFBV =
 
   let id_eunop = function
   | Unot -> 0
-  | Uneg -> Pervasives.succ 0
-  | Uextr (_, _) -> Pervasives.succ (Pervasives.succ 0)
+  | Uneg -> Stdlib.succ 0
+  | Uextr (_, _) -> Stdlib.succ (Stdlib.succ 0)
   | Uhigh _ ->
-    Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ 0)))
+    Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ 0)))
   | Ulow _ ->
-    Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ 0))))
+    Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ 0))))
   | Uzext _ ->
-    Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ 0)))))
+    Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ 0)))))
   | Usext _ ->
-    Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ (Pervasives.succ 0))))))
+    Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ (Stdlib.succ 0))))))
   | Urepeat _ ->
-    Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
+    Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
       0)))))))
   | Urotl _ ->
-    Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ 0))))))))
+    Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ 0))))))))
   | Urotr _ ->
-    Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ 0)))))))))
+    Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ 0)))))))))
 
   (** val eunop_ltn : eunop -> eunop -> bool **)
 
@@ -1330,177 +1330,177 @@ module MakeQFBV =
     | Uextr (i1, j1) ->
       (match o2 with
        | Uextr (i2, j2) ->
-         (||) (leq (Pervasives.succ i1) i2)
+         (||) (leq (Stdlib.succ i1) i2)
            ((&&) (eq_op nat_eqType (Obj.magic i1) (Obj.magic i2))
-             (leq (Pervasives.succ j1) j2))
-       | _ -> leq (Pervasives.succ (id_eunop o1)) (id_eunop o2))
+             (leq (Stdlib.succ j1) j2))
+       | _ -> leq (Stdlib.succ (id_eunop o1)) (id_eunop o2))
     | Uhigh n1 ->
       (match o2 with
-       | Uhigh n2 -> leq (Pervasives.succ n1) n2
-       | _ -> leq (Pervasives.succ (id_eunop o1)) (id_eunop o2))
+       | Uhigh n2 -> leq (Stdlib.succ n1) n2
+       | _ -> leq (Stdlib.succ (id_eunop o1)) (id_eunop o2))
     | Ulow n1 ->
       (match o2 with
-       | Ulow n2 -> leq (Pervasives.succ n1) n2
-       | _ -> leq (Pervasives.succ (id_eunop o1)) (id_eunop o2))
+       | Ulow n2 -> leq (Stdlib.succ n1) n2
+       | _ -> leq (Stdlib.succ (id_eunop o1)) (id_eunop o2))
     | Uzext n1 ->
       (match o2 with
-       | Uzext n2 -> leq (Pervasives.succ n1) n2
-       | _ -> leq (Pervasives.succ (id_eunop o1)) (id_eunop o2))
+       | Uzext n2 -> leq (Stdlib.succ n1) n2
+       | _ -> leq (Stdlib.succ (id_eunop o1)) (id_eunop o2))
     | Usext n1 ->
       (match o2 with
-       | Usext n2 -> leq (Pervasives.succ n1) n2
-       | _ -> leq (Pervasives.succ (id_eunop o1)) (id_eunop o2))
+       | Usext n2 -> leq (Stdlib.succ n1) n2
+       | _ -> leq (Stdlib.succ (id_eunop o1)) (id_eunop o2))
     | Urepeat n1 ->
       (match o2 with
-       | Urepeat n2 -> leq (Pervasives.succ n1) n2
-       | _ -> leq (Pervasives.succ (id_eunop o1)) (id_eunop o2))
+       | Urepeat n2 -> leq (Stdlib.succ n1) n2
+       | _ -> leq (Stdlib.succ (id_eunop o1)) (id_eunop o2))
     | Urotl n1 ->
       (match o2 with
-       | Urotl n2 -> leq (Pervasives.succ n1) n2
-       | _ -> leq (Pervasives.succ (id_eunop o1)) (id_eunop o2))
+       | Urotl n2 -> leq (Stdlib.succ n1) n2
+       | _ -> leq (Stdlib.succ (id_eunop o1)) (id_eunop o2))
     | Urotr n1 ->
       (match o2 with
-       | Urotr n2 -> leq (Pervasives.succ n1) n2
-       | _ -> leq (Pervasives.succ (id_eunop o1)) (id_eunop o2))
-    | _ -> leq (Pervasives.succ (id_eunop o1)) (id_eunop o2)
+       | Urotr n2 -> leq (Stdlib.succ n1) n2
+       | _ -> leq (Stdlib.succ (id_eunop o1)) (id_eunop o2))
+    | _ -> leq (Stdlib.succ (id_eunop o1)) (id_eunop o2)
 
   (** val id_ebinop : ebinop -> int **)
 
   let id_ebinop = function
   | Band -> 0
-  | Bor -> Pervasives.succ 0
-  | Bxor -> Pervasives.succ (Pervasives.succ 0)
-  | Badd -> Pervasives.succ (Pervasives.succ (Pervasives.succ 0))
+  | Bor -> Stdlib.succ 0
+  | Bxor -> Stdlib.succ (Stdlib.succ 0)
+  | Badd -> Stdlib.succ (Stdlib.succ (Stdlib.succ 0))
   | Bsub ->
-    Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ 0)))
+    Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ 0)))
   | Bmul ->
-    Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ 0))))
+    Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ 0))))
   | Bdiv ->
-    Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ 0)))))
+    Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ 0)))))
   | Bmod ->
-    Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ (Pervasives.succ 0))))))
+    Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ (Stdlib.succ 0))))))
   | Bsdiv ->
-    Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
+    Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
       0)))))))
   | Bsrem ->
-    Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ 0))))))))
+    Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ 0))))))))
   | Bsmod ->
-    Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ 0)))))))))
+    Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ 0)))))))))
   | Bshl ->
-    Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ (Pervasives.succ 0))))))))))
+    Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ (Stdlib.succ 0))))))))))
   | Blshr ->
-    Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
+    Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
       0)))))))))))
   | Bashr ->
-    Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ 0))))))))))))
+    Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ 0))))))))))))
   | Bconcat ->
-    Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ 0)))))))))))))
+    Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ 0)))))))))))))
   | Bcomp ->
-    Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ (Pervasives.succ 0))))))))))))))
+    Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ (Stdlib.succ 0))))))))))))))
 
   (** val ebinop_ltn : ebinop -> ebinop -> bool **)
 
   let ebinop_ltn o1 o2 =
-    leq (Pervasives.succ (id_ebinop o1)) (id_ebinop o2)
+    leq (Stdlib.succ (id_ebinop o1)) (id_ebinop o2)
 
   (** val id_bbinop : bbinop -> int **)
 
   let id_bbinop = function
   | Beq -> 0
-  | Bult -> Pervasives.succ 0
-  | Bule -> Pervasives.succ (Pervasives.succ 0)
-  | Bugt -> Pervasives.succ (Pervasives.succ (Pervasives.succ 0))
+  | Bult -> Stdlib.succ 0
+  | Bule -> Stdlib.succ (Stdlib.succ 0)
+  | Bugt -> Stdlib.succ (Stdlib.succ (Stdlib.succ 0))
   | Buge ->
-    Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ 0)))
+    Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ 0)))
   | Bslt ->
-    Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ 0))))
+    Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ 0))))
   | Bsle ->
-    Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ 0)))))
+    Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ 0)))))
   | Bsgt ->
-    Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ (Pervasives.succ 0))))))
+    Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ (Stdlib.succ 0))))))
   | Bsge ->
-    Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
+    Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
       0)))))))
   | Buaddo ->
-    Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ 0))))))))
+    Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ 0))))))))
   | Busubo ->
-    Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ 0)))))))))
+    Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ 0)))))))))
   | Bumulo ->
-    Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ (Pervasives.succ 0))))))))))
+    Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ (Stdlib.succ 0))))))))))
   | Bsaddo ->
-    Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
+    Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
       0)))))))))))
   | Bssubo ->
-    Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ 0))))))))))))
+    Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ 0))))))))))))
   | Bsmulo ->
-    Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ (Pervasives.succ 0)))))))))))))
+    Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ (Stdlib.succ 0)))))))))))))
 
   (** val bbinop_ltn : bbinop -> bbinop -> bool **)
 
   let bbinop_ltn o1 o2 =
-    leq (Pervasives.succ (id_bbinop o1)) (id_bbinop o2)
+    leq (Stdlib.succ (id_bbinop o1)) (id_bbinop o2)
 
   (** val id_exp : exp -> int **)
 
   let id_exp = function
   | Evar _ -> 0
-  | Econst _ -> Pervasives.succ 0
-  | Eunop (_, _) -> Pervasives.succ (Pervasives.succ 0)
-  | Ebinop (_, _, _) -> Pervasives.succ (Pervasives.succ (Pervasives.succ 0))
+  | Econst _ -> Stdlib.succ 0
+  | Eunop (_, _) -> Stdlib.succ (Stdlib.succ 0)
+  | Ebinop (_, _, _) -> Stdlib.succ (Stdlib.succ (Stdlib.succ 0))
   | Eite (_, _, _) ->
-    Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ 0)))
+    Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ 0)))
 
   (** val id_bexp : bexp -> int **)
 
   let id_bexp = function
   | Bfalse -> 0
-  | Btrue -> Pervasives.succ 0
-  | Bbinop (_, _, _) -> Pervasives.succ (Pervasives.succ 0)
-  | Blneg _ -> Pervasives.succ (Pervasives.succ (Pervasives.succ 0))
+  | Btrue -> Stdlib.succ 0
+  | Bbinop (_, _, _) -> Stdlib.succ (Stdlib.succ 0)
+  | Blneg _ -> Stdlib.succ (Stdlib.succ (Stdlib.succ 0))
   | Bconj (_, _) ->
-    Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ 0)))
+    Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ 0)))
   | Bdisj (_, _) ->
-    Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-      (Pervasives.succ 0))))
+    Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+      (Stdlib.succ 0))))
 
   (** val exp_ltn : exp -> exp -> bool **)
 
@@ -1509,21 +1509,21 @@ module MakeQFBV =
     | Evar v1 ->
       (match e2 with
        | Evar v2 -> V.ltn v1 v2
-       | _ -> leq (Pervasives.succ (id_exp e1)) (id_exp e2))
+       | _ -> leq (Stdlib.succ (id_exp e1)) (id_exp e2))
     | Econst n1 ->
       (match e2 with
        | Econst n2 ->
-         (||) (leq (Pervasives.succ (size n1)) (size n2))
+         (||) (leq (Stdlib.succ (size n1)) (size n2))
            ((&&) (eq_op nat_eqType (Obj.magic size n1) (Obj.magic size n2))
              (ltB_lsb n1 n2))
-       | _ -> leq (Pervasives.succ (id_exp e1)) (id_exp e2))
+       | _ -> leq (Stdlib.succ (id_exp e1)) (id_exp e2))
     | Eunop (o1, e3) ->
       (match e2 with
        | Eunop (o2, e4) ->
          (||) (eunop_ltn o1 o2)
            ((&&) (eq_op eunop_eqType (Obj.magic o1) (Obj.magic o2))
              (exp_ltn e3 e4))
-       | _ -> leq (Pervasives.succ (id_exp e1)) (id_exp e2))
+       | _ -> leq (Stdlib.succ (id_exp e1)) (id_exp e2))
     | Ebinop (o1, e3, e4) ->
       (match e2 with
        | Ebinop (o2, e5, e6) ->
@@ -1535,7 +1535,7 @@ module MakeQFBV =
              ((&&) (eq_op ebinop_eqType (Obj.magic o1) (Obj.magic o2))
                (eq_op exp_eqType (Obj.magic e3) (Obj.magic e5)))
              (exp_ltn e4 e6))
-       | _ -> leq (Pervasives.succ (id_exp e1)) (id_exp e2))
+       | _ -> leq (Stdlib.succ (id_exp e1)) (id_exp e2))
     | Eite (c1, e3, e4) ->
       (match e2 with
        | Eite (c2, e5, e6) ->
@@ -1547,7 +1547,7 @@ module MakeQFBV =
              ((&&) (eq_op bexp_eqType (Obj.magic c1) (Obj.magic c2))
                (eq_op exp_eqType (Obj.magic e3) (Obj.magic e5)))
              (exp_ltn e4 e6))
-       | _ -> leq (Pervasives.succ (id_exp e1)) (id_exp e2))
+       | _ -> leq (Stdlib.succ (id_exp e1)) (id_exp e2))
 
   (** val bexp_ltn : bexp -> bexp -> bool **)
 
@@ -1564,26 +1564,26 @@ module MakeQFBV =
              ((&&) (eq_op bbinop_eqType (Obj.magic o1) (Obj.magic o2))
                (eq_op exp_eqType (Obj.magic e3) (Obj.magic e5)))
              (exp_ltn e4 e6))
-       | _ -> leq (Pervasives.succ (id_bexp e1)) (id_bexp e2))
+       | _ -> leq (Stdlib.succ (id_bexp e1)) (id_bexp e2))
     | Blneg e3 ->
       (match e2 with
        | Blneg e4 -> bexp_ltn e3 e4
-       | _ -> leq (Pervasives.succ (id_bexp e1)) (id_bexp e2))
+       | _ -> leq (Stdlib.succ (id_bexp e1)) (id_bexp e2))
     | Bconj (e3, e4) ->
       (match e2 with
        | Bconj (e5, e6) ->
          (||) (bexp_ltn e3 e5)
            ((&&) (eq_op bexp_eqType (Obj.magic e3) (Obj.magic e5))
              (bexp_ltn e4 e6))
-       | _ -> leq (Pervasives.succ (id_bexp e1)) (id_bexp e2))
+       | _ -> leq (Stdlib.succ (id_bexp e1)) (id_bexp e2))
     | Bdisj (e3, e4) ->
       (match e2 with
        | Bdisj (e5, e6) ->
          (||) (bexp_ltn e3 e5)
            ((&&) (eq_op bexp_eqType (Obj.magic e3) (Obj.magic e5))
              (bexp_ltn e4 e6))
-       | _ -> leq (Pervasives.succ (id_bexp e1)) (id_bexp e2))
-    | _ -> leq (Pervasives.succ (id_bexp e1)) (id_bexp e2)
+       | _ -> leq (Stdlib.succ (id_bexp e1)) (id_bexp e2))
+    | _ -> leq (Stdlib.succ (id_bexp e1)) (id_bexp e2)
 
   (** val exp_compare : exp -> exp -> exp OrderedType.coq_Compare **)
 
@@ -1668,20 +1668,20 @@ module MakeQFBV =
   (** val len_exp : exp -> int **)
 
   let rec len_exp = function
-  | Eunop (_, e0) -> Pervasives.succ (len_exp e0)
-  | Ebinop (_, e1, e2) -> Pervasives.succ (addn (len_exp e1) (len_exp e2))
+  | Eunop (_, e0) -> Stdlib.succ (len_exp e0)
+  | Ebinop (_, e1, e2) -> Stdlib.succ (addn (len_exp e1) (len_exp e2))
   | Eite (b, e1, e2) ->
-    Pervasives.succ (addn (addn (len_bexp b) (len_exp e1)) (len_exp e2))
-  | _ -> Pervasives.succ 0
+    Stdlib.succ (addn (addn (len_bexp b) (len_exp e1)) (len_exp e2))
+  | _ -> Stdlib.succ 0
 
   (** val len_bexp : bexp -> int **)
 
   and len_bexp = function
-  | Bbinop (_, e1, e2) -> Pervasives.succ (addn (len_exp e1) (len_exp e2))
-  | Blneg e0 -> Pervasives.succ (len_bexp e0)
-  | Bconj (e1, e2) -> Pervasives.succ (addn (len_bexp e1) (len_bexp e2))
-  | Bdisj (e1, e2) -> Pervasives.succ (addn (len_bexp e1) (len_bexp e2))
-  | _ -> Pervasives.succ 0
+  | Bbinop (_, e1, e2) -> Stdlib.succ (addn (len_exp e1) (len_exp e2))
+  | Blneg e0 -> Stdlib.succ (len_bexp e0)
+  | Bconj (e1, e2) -> Stdlib.succ (addn (len_bexp e1) (len_bexp e2))
+  | Bdisj (e1, e2) -> Stdlib.succ (addn (len_bexp e1) (len_bexp e2))
+  | _ -> Stdlib.succ 0
 
   (** val subee : exp -> exp -> bool **)
 
@@ -1731,7 +1731,7 @@ module MakeQFBV =
     | Econst n -> size n
     | Eunop (op0, e0) ->
       (match op0 with
-       | Uextr (i, j) -> addn (subn i j) (Pervasives.succ 0)
+       | Uextr (i, j) -> addn (subn i j) (Stdlib.succ 0)
        | Uhigh n -> n
        | Ulow n -> n
        | Uzext n -> addn (exp_size e0 te) n
@@ -1746,7 +1746,7 @@ module MakeQFBV =
        | Badd -> minn (exp_size e1 te) (exp_size e2 te)
        | Bsub -> minn (exp_size e1 te) (exp_size e2 te)
        | Bconcat -> addn (exp_size e1 te) (exp_size e2 te)
-       | Bcomp -> Pervasives.succ 0
+       | Bcomp -> Stdlib.succ 0
        | _ -> exp_size e1 te)
     | Eite (_, e1, e2) -> maxn (exp_size e1 te) (exp_size e2 te)
 
@@ -1760,7 +1760,7 @@ module MakeQFBV =
     | Ebinop (op0, e1, e2) ->
       (&&)
         ((&&) ((&&) (well_formed_exp e1 te) (well_formed_exp e2 te))
-          (leq (Pervasives.succ 0) (exp_size e1 te)))
+          (leq (Stdlib.succ 0) (exp_size e1 te)))
         (if eq_op ebinop_eqType (Obj.magic op0) (Obj.magic Bconcat)
          then true
          else eq_op nat_eqType (Obj.magic exp_size e1 te)
diff --git a/src/ocaml/extraction/QFBVHash.ml b/src/ocaml/extraction/QFBVHash.ml
index 1f1d278..564416b 100644
--- a/src/ocaml/extraction/QFBVHash.ml
+++ b/src/ocaml/extraction/QFBVHash.ml
@@ -201,24 +201,24 @@ let hbexp_eqType =
 
 let id_hashed_exp = function
 | HEvar _ -> 0
-| HEconst _ -> Pervasives.succ 0
-| HEunop (_, _) -> Pervasives.succ (Pervasives.succ 0)
-| HEbinop (_, _, _) -> Pervasives.succ (Pervasives.succ (Pervasives.succ 0))
+| HEconst _ -> Stdlib.succ 0
+| HEunop (_, _) -> Stdlib.succ (Stdlib.succ 0)
+| HEbinop (_, _, _) -> Stdlib.succ (Stdlib.succ (Stdlib.succ 0))
 | HEite (_, _, _) ->
-  Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ 0)))
+  Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ 0)))
 
 (** val id_hashed_bexp : hashed_bexp -> int **)
 
 let id_hashed_bexp = function
 | HBfalse -> 0
-| HBtrue -> Pervasives.succ 0
-| HBbinop (_, _, _) -> Pervasives.succ (Pervasives.succ 0)
-| HBlneg _ -> Pervasives.succ (Pervasives.succ (Pervasives.succ 0))
+| HBtrue -> Stdlib.succ 0
+| HBbinop (_, _, _) -> Stdlib.succ (Stdlib.succ 0)
+| HBlneg _ -> Stdlib.succ (Stdlib.succ (Stdlib.succ 0))
 | HBconj (_, _) ->
-  Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ 0)))
+  Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ 0)))
 | HBdisj (_, _) ->
-  Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
-    (Pervasives.succ 0))))
+  Stdlib.succ (Stdlib.succ (Stdlib.succ (Stdlib.succ
+    (Stdlib.succ 0))))
 
 (** val sizen : bits -> coq_N **)
 
@@ -233,7 +233,7 @@ let rec hashed_exp_ltn e1 e2 =
   | HEvar v1 ->
     (match e2 with
      | HEvar v2 -> SSAVarOrder.ltn v1 v2
-     | _ -> leq (Pervasives.succ (id_hashed_exp e1)) (id_hashed_exp e2))
+     | _ -> leq (Stdlib.succ (id_hashed_exp e1)) (id_hashed_exp e2))
   | HEconst n1 ->
     (match e2 with
      | HEconst n2 ->
@@ -241,14 +241,14 @@ let rec hashed_exp_ltn e1 e2 =
          ((&&)
            (eq_op bin_nat_eqType (Obj.magic sizen n1) (Obj.magic sizen n2))
            (ltB_lsb n1 n2))
-     | _ -> leq (Pervasives.succ (id_hashed_exp e1)) (id_hashed_exp e2))
+     | _ -> leq (Stdlib.succ (id_hashed_exp e1)) (id_hashed_exp e2))
   | HEunop (o1, f1) ->
     (match e2 with
      | HEunop (o2, f2) ->
        (||) (QFBV.QFBV.eunop_ltn o1 o2)
          ((&&) (eq_op QFBV.eunop_eqType (Obj.magic o1) (Obj.magic o2))
            (hexp_ltn f1 f2))
-     | _ -> leq (Pervasives.succ (id_hashed_exp e1)) (id_hashed_exp e2))
+     | _ -> leq (Stdlib.succ (id_hashed_exp e1)) (id_hashed_exp e2))
   | HEbinop (o1, f1, f2) ->
     (match e2 with
      | HEbinop (o2, f3, f4) ->
@@ -260,7 +260,7 @@ let rec hashed_exp_ltn e1 e2 =
            ((&&) (eq_op QFBV.ebinop_eqType (Obj.magic o1) (Obj.magic o2))
              (eq_op hexp_eqType (Obj.magic f1) (Obj.magic f3)))
            (hexp_ltn f2 f4))
-     | _ -> leq (Pervasives.succ (id_hashed_exp e1)) (id_hashed_exp e2))
+     | _ -> leq (Stdlib.succ (id_hashed_exp e1)) (id_hashed_exp e2))
   | HEite (c1, f1, f2) ->
     (match e2 with
      | HEite (c2, f3, f4) ->
@@ -272,7 +272,7 @@ let rec hashed_exp_ltn e1 e2 =
            ((&&) (eq_op hbexp_eqType (Obj.magic c1) (Obj.magic c2))
              (eq_op hexp_eqType (Obj.magic f1) (Obj.magic f3)))
            (hexp_ltn f2 f4))
-     | _ -> leq (Pervasives.succ (id_hashed_exp e1)) (id_hashed_exp e2))
+     | _ -> leq (Stdlib.succ (id_hashed_exp e1)) (id_hashed_exp e2))
 
 (** val hashed_bexp_ltn : hashed_bexp -> hashed_bexp -> bool **)
 
@@ -289,26 +289,26 @@ and hashed_bexp_ltn e1 e2 =
            ((&&) (eq_op QFBV.bbinop_eqType (Obj.magic o1) (Obj.magic o2))
              (eq_op hexp_eqType (Obj.magic f1) (Obj.magic f3)))
            (hexp_ltn f2 f4))
-     | _ -> leq (Pervasives.succ (id_hashed_bexp e1)) (id_hashed_bexp e2))
+     | _ -> leq (Stdlib.succ (id_hashed_bexp e1)) (id_hashed_bexp e2))
   | HBlneg f1 ->
     (match e2 with
      | HBlneg f2 -> hbexp_ltn f1 f2
-     | _ -> leq (Pervasives.succ (id_hashed_bexp e1)) (id_hashed_bexp e2))
+     | _ -> leq (Stdlib.succ (id_hashed_bexp e1)) (id_hashed_bexp e2))
   | HBconj (f1, f2) ->
     (match e2 with
      | HBconj (f3, f4) ->
        (||) (hbexp_ltn f1 f3)
          ((&&) (eq_op hbexp_eqType (Obj.magic f1) (Obj.magic f3))
            (hbexp_ltn f2 f4))
-     | _ -> leq (Pervasives.succ (id_hashed_bexp e1)) (id_hashed_bexp e2))
+     | _ -> leq (Stdlib.succ (id_hashed_bexp e1)) (id_hashed_bexp e2))
   | HBdisj (f1, f2) ->
     (match e2 with
      | HBdisj (f3, f4) ->
        (||) (hbexp_ltn f1 f3)
          ((&&) (eq_op hbexp_eqType (Obj.magic f1) (Obj.magic f3))
            (hbexp_ltn f2 f4))
-     | _ -> leq (Pervasives.succ (id_hashed_bexp e1)) (id_hashed_bexp e2))
-  | _ -> leq (Pervasives.succ (id_hashed_bexp e1)) (id_hashed_bexp e2)
+     | _ -> leq (Stdlib.succ (id_hashed_bexp e1)) (id_hashed_bexp e2))
+  | _ -> leq (Stdlib.succ (id_hashed_bexp e1)) (id_hashed_bexp e2)
 
 (** val hexp_ltn : hexp -> hexp -> bool **)
 
diff --git a/src/ocaml/extraction/REP.ml b/src/ocaml/extraction/REP.ml
index 5872cbc..d8e54c4 100644
--- a/src/ocaml/extraction/REP.ml
+++ b/src/ocaml/extraction/REP.ml
@@ -136,7 +136,7 @@ let rec single_variables = function
 (** val num_occurrence : SSAVarOrder.t -> SSALite.SSALite.eexp -> int **)
 
 let rec num_occurrence v = function
-| Evar x -> if eq_op SSAVarOrder.coq_T x v then Pervasives.succ 0 else 0
+| Evar x -> if eq_op SSAVarOrder.coq_T x v then Stdlib.succ 0 else 0
 | Econst _ -> 0
 | Eunop (_, e0) -> num_occurrence v e0
 | Ebinop (_, e1, e2) -> addn (num_occurrence v e1) (num_occurrence v e2)
@@ -175,7 +175,7 @@ let get_rewrite_pattern e =
   let candidates =
     SSAVS.filter (fun v ->
       eq_op nat_eqType (Obj.magic num_occurrence v e)
-        (Obj.magic (Pervasives.succ 0))) (single_variables e)
+        (Obj.magic (Stdlib.succ 0))) (single_variables e)
   in
   if eq_op nat_eqType (Obj.magic SSAVS.cardinal candidates) (Obj.magic 0)
   then None
diff --git a/src/ocaml/extraction/SSA2QFBV.ml b/src/ocaml/extraction/SSA2QFBV.ml
index 61dc8b0..4acb0f1 100644
--- a/src/ocaml/extraction/SSA2QFBV.ml
+++ b/src/ocaml/extraction/SSA2QFBV.ml
@@ -89,7 +89,7 @@ let bexp_instr e = function
 | SSALite.SSALite.Icmov (v, c, a1, a2) ->
   QFBV.QFBV.qfbv_eq (QFBV.QFBV.qfbv_var v) (QFBV.QFBV.Eite
     ((QFBV.QFBV.qfbv_eq
-       (QFBV.QFBV.qfbv_const (Pervasives.succ 0) (Pervasives.succ 0))
+       (QFBV.QFBV.qfbv_const (Stdlib.succ 0) (Stdlib.succ 0))
        (qfbv_atom c)), (qfbv_atom a1), (qfbv_atom a2)))
 | SSALite.SSALite.Inot (v, _, a) ->
   QFBV.QFBV.qfbv_eq (QFBV.QFBV.qfbv_var v) (QFBV.QFBV.qfbv_not (qfbv_atom a))
@@ -99,38 +99,38 @@ let bexp_instr e = function
 | SSALite.SSALite.Iadds (c, v, a1, a2) ->
   QFBV.QFBV.qfbv_conj
     (QFBV.QFBV.qfbv_eq (QFBV.QFBV.qfbv_var c)
-      (QFBV.QFBV.qfbv_high (Pervasives.succ 0)
+      (QFBV.QFBV.qfbv_high (Stdlib.succ 0)
         (QFBV.QFBV.qfbv_add
-          (QFBV.QFBV.qfbv_zext (Pervasives.succ 0) (qfbv_atom a1))
-          (QFBV.QFBV.qfbv_zext (Pervasives.succ 0) (qfbv_atom a2)))))
+          (QFBV.QFBV.qfbv_zext (Stdlib.succ 0) (qfbv_atom a1))
+          (QFBV.QFBV.qfbv_zext (Stdlib.succ 0) (qfbv_atom a2)))))
     (QFBV.QFBV.qfbv_eq (QFBV.QFBV.qfbv_var v)
       (QFBV.QFBV.qfbv_low (SSALite.SSALite.asize a1 e)
         (QFBV.QFBV.qfbv_add
-          (QFBV.QFBV.qfbv_zext (Pervasives.succ 0) (qfbv_atom a1))
-          (QFBV.QFBV.qfbv_zext (Pervasives.succ 0) (qfbv_atom a2)))))
+          (QFBV.QFBV.qfbv_zext (Stdlib.succ 0) (qfbv_atom a1))
+          (QFBV.QFBV.qfbv_zext (Stdlib.succ 0) (qfbv_atom a2)))))
 | SSALite.SSALite.Iadc (v, a1, a2, y) ->
   QFBV.QFBV.qfbv_eq (QFBV.QFBV.qfbv_var v)
     (QFBV.QFBV.qfbv_low (SSALite.SSALite.asize a1 e)
       (QFBV.QFBV.qfbv_add
         (QFBV.QFBV.qfbv_add
-          (QFBV.QFBV.qfbv_zext (Pervasives.succ 0) (qfbv_atom a1))
-          (QFBV.QFBV.qfbv_zext (Pervasives.succ 0) (qfbv_atom a2)))
+          (QFBV.QFBV.qfbv_zext (Stdlib.succ 0) (qfbv_atom a1))
+          (QFBV.QFBV.qfbv_zext (Stdlib.succ 0) (qfbv_atom a2)))
         (QFBV.QFBV.qfbv_zext (SSALite.SSALite.asize a1 e) (qfbv_atom y))))
 | SSALite.SSALite.Iadcs (c, v, a1, a2, y) ->
   QFBV.QFBV.qfbv_conj
     (QFBV.QFBV.qfbv_eq (QFBV.QFBV.qfbv_var c)
-      (QFBV.QFBV.qfbv_high (Pervasives.succ 0)
+      (QFBV.QFBV.qfbv_high (Stdlib.succ 0)
         (QFBV.QFBV.qfbv_add
           (QFBV.QFBV.qfbv_add
-            (QFBV.QFBV.qfbv_zext (Pervasives.succ 0) (qfbv_atom a1))
-            (QFBV.QFBV.qfbv_zext (Pervasives.succ 0) (qfbv_atom a2)))
+            (QFBV.QFBV.qfbv_zext (Stdlib.succ 0) (qfbv_atom a1))
+            (QFBV.QFBV.qfbv_zext (Stdlib.succ 0) (qfbv_atom a2)))
           (QFBV.QFBV.qfbv_zext (SSALite.SSALite.asize a1 e) (qfbv_atom y)))))
     (QFBV.QFBV.qfbv_eq (QFBV.QFBV.qfbv_var v)
       (QFBV.QFBV.qfbv_low (SSALite.SSALite.asize a1 e)
         (QFBV.QFBV.qfbv_add
           (QFBV.QFBV.qfbv_add
-            (QFBV.QFBV.qfbv_zext (Pervasives.succ 0) (qfbv_atom a1))
-            (QFBV.QFBV.qfbv_zext (Pervasives.succ 0) (qfbv_atom a2)))
+            (QFBV.QFBV.qfbv_zext (Stdlib.succ 0) (qfbv_atom a1))
+            (QFBV.QFBV.qfbv_zext (Stdlib.succ 0) (qfbv_atom a2)))
           (QFBV.QFBV.qfbv_zext (SSALite.SSALite.asize a1 e) (qfbv_atom y)))))
 | SSALite.SSALite.Isub (v, a1, a2) ->
   QFBV.QFBV.qfbv_eq (QFBV.QFBV.qfbv_var v)
@@ -138,60 +138,60 @@ let bexp_instr e = function
 | SSALite.SSALite.Isubc (c, v, a1, a2) ->
   QFBV.QFBV.qfbv_conj
     (QFBV.QFBV.qfbv_eq (QFBV.QFBV.qfbv_var c)
-      (QFBV.QFBV.qfbv_high (Pervasives.succ 0)
+      (QFBV.QFBV.qfbv_high (Stdlib.succ 0)
         (QFBV.QFBV.qfbv_add
           (QFBV.QFBV.qfbv_add
-            (QFBV.QFBV.qfbv_zext (Pervasives.succ 0) (qfbv_atom a1))
-            (QFBV.QFBV.qfbv_zext (Pervasives.succ 0)
+            (QFBV.QFBV.qfbv_zext (Stdlib.succ 0) (qfbv_atom a1))
+            (QFBV.QFBV.qfbv_zext (Stdlib.succ 0)
               (QFBV.QFBV.qfbv_not (qfbv_atom a2))))
           (QFBV.QFBV.qfbv_zext (SSALite.SSALite.asize a1 e)
-            (QFBV.QFBV.qfbv_const (Pervasives.succ 0) (Pervasives.succ 0))))))
+            (QFBV.QFBV.qfbv_const (Stdlib.succ 0) (Stdlib.succ 0))))))
     (QFBV.QFBV.qfbv_eq (QFBV.QFBV.qfbv_var v)
       (QFBV.QFBV.qfbv_low (SSALite.SSALite.asize a1 e)
         (QFBV.QFBV.qfbv_add
           (QFBV.QFBV.qfbv_add
-            (QFBV.QFBV.qfbv_zext (Pervasives.succ 0) (qfbv_atom a1))
-            (QFBV.QFBV.qfbv_zext (Pervasives.succ 0)
+            (QFBV.QFBV.qfbv_zext (Stdlib.succ 0) (qfbv_atom a1))
+            (QFBV.QFBV.qfbv_zext (Stdlib.succ 0)
               (QFBV.QFBV.qfbv_not (qfbv_atom a2))))
           (QFBV.QFBV.qfbv_zext (SSALite.SSALite.asize a1 e)
-            (QFBV.QFBV.qfbv_const (Pervasives.succ 0) (Pervasives.succ 0))))))
+            (QFBV.QFBV.qfbv_const (Stdlib.succ 0) (Stdlib.succ 0))))))
 | SSALite.SSALite.Isubb (b, v, a1, a2) ->
   QFBV.QFBV.qfbv_conj
     (QFBV.QFBV.qfbv_eq (QFBV.QFBV.qfbv_var b)
-      (QFBV.QFBV.qfbv_high (Pervasives.succ 0)
+      (QFBV.QFBV.qfbv_high (Stdlib.succ 0)
         (QFBV.QFBV.qfbv_sub
-          (QFBV.QFBV.qfbv_zext (Pervasives.succ 0) (qfbv_atom a1))
-          (QFBV.QFBV.qfbv_zext (Pervasives.succ 0) (qfbv_atom a2)))))
+          (QFBV.QFBV.qfbv_zext (Stdlib.succ 0) (qfbv_atom a1))
+          (QFBV.QFBV.qfbv_zext (Stdlib.succ 0) (qfbv_atom a2)))))
     (QFBV.QFBV.qfbv_eq (QFBV.QFBV.qfbv_var v)
       (QFBV.QFBV.qfbv_low (SSALite.SSALite.asize a1 e)
         (QFBV.QFBV.qfbv_sub
-          (QFBV.QFBV.qfbv_zext (Pervasives.succ 0) (qfbv_atom a1))
-          (QFBV.QFBV.qfbv_zext (Pervasives.succ 0) (qfbv_atom a2)))))
+          (QFBV.QFBV.qfbv_zext (Stdlib.succ 0) (qfbv_atom a1))
+          (QFBV.QFBV.qfbv_zext (Stdlib.succ 0) (qfbv_atom a2)))))
 | SSALite.SSALite.Isbc (v, a1, a2, y) ->
   QFBV.QFBV.qfbv_eq (QFBV.QFBV.qfbv_var v)
     (QFBV.QFBV.qfbv_low (SSALite.SSALite.asize a1 e)
       (QFBV.QFBV.qfbv_add
         (QFBV.QFBV.qfbv_add
-          (QFBV.QFBV.qfbv_zext (Pervasives.succ 0) (qfbv_atom a1))
-          (QFBV.QFBV.qfbv_zext (Pervasives.succ 0)
+          (QFBV.QFBV.qfbv_zext (Stdlib.succ 0) (qfbv_atom a1))
+          (QFBV.QFBV.qfbv_zext (Stdlib.succ 0)
             (QFBV.QFBV.qfbv_not (qfbv_atom a2))))
         (QFBV.QFBV.qfbv_zext (SSALite.SSALite.asize a1 e) (qfbv_atom y))))
 | SSALite.SSALite.Isbcs (c, v, a1, a2, y) ->
   QFBV.QFBV.qfbv_conj
     (QFBV.QFBV.qfbv_eq (QFBV.QFBV.qfbv_var c)
-      (QFBV.QFBV.qfbv_high (Pervasives.succ 0)
+      (QFBV.QFBV.qfbv_high (Stdlib.succ 0)
         (QFBV.QFBV.qfbv_add
           (QFBV.QFBV.qfbv_add
-            (QFBV.QFBV.qfbv_zext (Pervasives.succ 0) (qfbv_atom a1))
-            (QFBV.QFBV.qfbv_zext (Pervasives.succ 0)
+            (QFBV.QFBV.qfbv_zext (Stdlib.succ 0) (qfbv_atom a1))
+            (QFBV.QFBV.qfbv_zext (Stdlib.succ 0)
               (QFBV.QFBV.qfbv_not (qfbv_atom a2))))
           (QFBV.QFBV.qfbv_zext (SSALite.SSALite.asize a1 e) (qfbv_atom y)))))
     (QFBV.QFBV.qfbv_eq (QFBV.QFBV.qfbv_var v)
       (QFBV.QFBV.qfbv_low (SSALite.SSALite.asize a1 e)
         (QFBV.QFBV.qfbv_add
           (QFBV.QFBV.qfbv_add
-            (QFBV.QFBV.qfbv_zext (Pervasives.succ 0) (qfbv_atom a1))
-            (QFBV.QFBV.qfbv_zext (Pervasives.succ 0)
+            (QFBV.QFBV.qfbv_zext (Stdlib.succ 0) (qfbv_atom a1))
+            (QFBV.QFBV.qfbv_zext (Stdlib.succ 0)
               (QFBV.QFBV.qfbv_not (qfbv_atom a2))))
           (QFBV.QFBV.qfbv_zext (SSALite.SSALite.asize a1 e) (qfbv_atom y)))))
 | SSALite.SSALite.Isbb (v, a1, a2, y) ->
@@ -199,24 +199,24 @@ let bexp_instr e = function
     (QFBV.QFBV.qfbv_low (SSALite.SSALite.asize a1 e)
       (QFBV.QFBV.qfbv_sub
         (QFBV.QFBV.qfbv_sub
-          (QFBV.QFBV.qfbv_zext (Pervasives.succ 0) (qfbv_atom a1))
-          (QFBV.QFBV.qfbv_zext (Pervasives.succ 0) (qfbv_atom a2)))
+          (QFBV.QFBV.qfbv_zext (Stdlib.succ 0) (qfbv_atom a1))
+          (QFBV.QFBV.qfbv_zext (Stdlib.succ 0) (qfbv_atom a2)))
         (QFBV.QFBV.qfbv_zext (SSALite.SSALite.asize a1 e) (qfbv_atom y))))
 | SSALite.SSALite.Isbbs (b, v, a1, a2, y) ->
   QFBV.QFBV.qfbv_conj
     (QFBV.QFBV.qfbv_eq (QFBV.QFBV.qfbv_var b)
-      (QFBV.QFBV.qfbv_high (Pervasives.succ 0)
+      (QFBV.QFBV.qfbv_high (Stdlib.succ 0)
         (QFBV.QFBV.qfbv_sub
           (QFBV.QFBV.qfbv_sub
-            (QFBV.QFBV.qfbv_zext (Pervasives.succ 0) (qfbv_atom a1))
-            (QFBV.QFBV.qfbv_zext (Pervasives.succ 0) (qfbv_atom a2)))
+            (QFBV.QFBV.qfbv_zext (Stdlib.succ 0) (qfbv_atom a1))
+            (QFBV.QFBV.qfbv_zext (Stdlib.succ 0) (qfbv_atom a2)))
           (QFBV.QFBV.qfbv_zext (SSALite.SSALite.asize a1 e) (qfbv_atom y)))))
     (QFBV.QFBV.qfbv_eq (QFBV.QFBV.qfbv_var v)
       (QFBV.QFBV.qfbv_low (SSALite.SSALite.asize a1 e)
         (QFBV.QFBV.qfbv_sub
           (QFBV.QFBV.qfbv_sub
-            (QFBV.QFBV.qfbv_zext (Pervasives.succ 0) (qfbv_atom a1))
-            (QFBV.QFBV.qfbv_zext (Pervasives.succ 0) (qfbv_atom a2)))
+            (QFBV.QFBV.qfbv_zext (Stdlib.succ 0) (qfbv_atom a1))
+            (QFBV.QFBV.qfbv_zext (Stdlib.succ 0) (qfbv_atom a2)))
           (QFBV.QFBV.qfbv_zext (SSALite.SSALite.asize a1 e) (qfbv_atom y)))))
 | SSALite.SSALite.Imul (v, a1, a2) ->
   QFBV.QFBV.qfbv_eq (QFBV.QFBV.qfbv_var v)
@@ -297,7 +297,7 @@ let bexp_instr e = function
      then if eq_op nat_eqType (Obj.magic sizeof_typ t)
                (Obj.magic sizeof_typ (SSALite.SSALite.atyp a e))
           then qfbv_atom a
-          else if leq (Pervasives.succ (sizeof_typ t))
+          else if leq (Stdlib.succ (sizeof_typ t))
                     (sizeof_typ (SSALite.SSALite.atyp a e))
                then QFBV.QFBV.qfbv_low (sizeof_typ t) (qfbv_atom a)
                else QFBV.QFBV.qfbv_zext
@@ -306,7 +306,7 @@ let bexp_instr e = function
      else if eq_op nat_eqType (Obj.magic sizeof_typ t)
                (Obj.magic sizeof_typ (SSALite.SSALite.atyp a e))
           then qfbv_atom a
-          else if leq (Pervasives.succ (sizeof_typ t))
+          else if leq (Stdlib.succ (sizeof_typ t))
                     (sizeof_typ (SSALite.SSALite.atyp a e))
                then QFBV.QFBV.qfbv_low (sizeof_typ t) (qfbv_atom a)
                else QFBV.QFBV.qfbv_sext
@@ -318,7 +318,7 @@ let bexp_instr e = function
      then if eq_op nat_eqType (Obj.magic sizeof_typ t)
                (Obj.magic sizeof_typ (SSALite.SSALite.atyp a e))
           then qfbv_atom a
-          else if leq (Pervasives.succ (sizeof_typ t))
+          else if leq (Stdlib.succ (sizeof_typ t))
                     (sizeof_typ (SSALite.SSALite.atyp a e))
                then QFBV.QFBV.qfbv_low (sizeof_typ t) (qfbv_atom a)
                else QFBV.QFBV.qfbv_zext
@@ -327,7 +327,7 @@ let bexp_instr e = function
      else if eq_op nat_eqType (Obj.magic sizeof_typ t)
                (Obj.magic sizeof_typ (SSALite.SSALite.atyp a e))
           then qfbv_atom a
-          else if leq (Pervasives.succ (sizeof_typ t))
+          else if leq (Stdlib.succ (sizeof_typ t))
                     (sizeof_typ (SSALite.SSALite.atyp a e))
                then QFBV.QFBV.qfbv_low (sizeof_typ t) (qfbv_atom a)
                else QFBV.QFBV.qfbv_sext
@@ -437,7 +437,7 @@ let bexp_atom_uadcB_algsnd a_size a1 a2 ac =
       (QFBV.QFBV.qfbv_lneg
         (QFBV.QFBV.qfbv_uaddo
           (QFBV.QFBV.qfbv_add (qfbv_atom a1) (qfbv_atom a2))
-          (QFBV.QFBV.qfbv_zext (subn a_size (Pervasives.succ 0))
+          (QFBV.QFBV.qfbv_zext (subn a_size (Stdlib.succ 0))
             (qfbv_atom ac))))
   | Aconst (_, bs1) ->
     (match a2 with
@@ -448,7 +448,7 @@ let bexp_atom_uadcB_algsnd a_size a1 a2 ac =
          (QFBV.QFBV.qfbv_lneg
            (QFBV.QFBV.qfbv_uaddo
              (QFBV.QFBV.qfbv_add (qfbv_atom a1) (qfbv_atom a2))
-             (QFBV.QFBV.qfbv_zext (subn a_size (Pervasives.succ 0))
+             (QFBV.QFBV.qfbv_zext (subn a_size (Stdlib.succ 0))
                (qfbv_atom ac))))
      | Aconst (_, bs2) ->
        (match ac with
@@ -456,16 +456,16 @@ let bexp_atom_uadcB_algsnd a_size a1 a2 ac =
           if coq_Uaddo bs1 bs2
           then QFBV.QFBV.qfbv_false
           else if coq_Uaddo (addB bs1 bs2)
-                    (zext (subn a_size (Pervasives.succ 0)) (b1 :: []))
+                    (zext (subn a_size (Stdlib.succ 0)) (b1 :: []))
                then QFBV.QFBV.qfbv_lneg
                       (QFBV.QFBV.qfbv_uaddo (QFBV.QFBV.Econst (addB bs1 bs2))
                         (QFBV.QFBV.qfbv_zext
-                          (subn a_size (Pervasives.succ 0)) (qfbv_atom ac)))
+                          (subn a_size (Stdlib.succ 0)) (qfbv_atom ac)))
                else QFBV.QFBV.qfbv_true
         | Aconst (_, c) ->
           if (||) (coq_Uaddo bs1 bs2)
                (coq_Uaddo (addB bs1 bs2)
-                 (zext (subn a_size (Pervasives.succ 0)) c))
+                 (zext (subn a_size (Stdlib.succ 0)) c))
           then QFBV.QFBV.qfbv_false
           else QFBV.QFBV.qfbv_true))
 
@@ -481,7 +481,7 @@ let bexp_atom_sadcB_algsnd a_size a1 a2 ac =
       (QFBV.QFBV.qfbv_lneg
         (QFBV.QFBV.qfbv_saddo
           (QFBV.QFBV.qfbv_add (qfbv_atom a1) (qfbv_atom a2))
-          (QFBV.QFBV.qfbv_zext (subn a_size (Pervasives.succ 0))
+          (QFBV.QFBV.qfbv_zext (subn a_size (Stdlib.succ 0))
             (qfbv_atom ac))))
   | Aconst (_, bs1) ->
     (match a2 with
@@ -492,7 +492,7 @@ let bexp_atom_sadcB_algsnd a_size a1 a2 ac =
          (QFBV.QFBV.qfbv_lneg
            (QFBV.QFBV.qfbv_saddo
              (QFBV.QFBV.qfbv_add (qfbv_atom a1) (qfbv_atom a2))
-             (QFBV.QFBV.qfbv_zext (subn a_size (Pervasives.succ 0))
+             (QFBV.QFBV.qfbv_zext (subn a_size (Stdlib.succ 0))
                (qfbv_atom ac))))
      | Aconst (_, bs2) ->
        (match ac with
@@ -500,16 +500,16 @@ let bexp_atom_sadcB_algsnd a_size a1 a2 ac =
           if coq_Saddo bs1 bs2
           then QFBV.QFBV.qfbv_false
           else if coq_Saddo (addB bs1 bs2)
-                    (zext (subn a_size (Pervasives.succ 0)) (b1 :: []))
+                    (zext (subn a_size (Stdlib.succ 0)) (b1 :: []))
                then QFBV.QFBV.qfbv_lneg
                       (QFBV.QFBV.qfbv_saddo (QFBV.QFBV.Econst (addB bs1 bs2))
                         (QFBV.QFBV.qfbv_zext
-                          (subn a_size (Pervasives.succ 0)) (qfbv_atom ac)))
+                          (subn a_size (Stdlib.succ 0)) (qfbv_atom ac)))
                else QFBV.QFBV.qfbv_true
         | Aconst (_, c) ->
           if (||) (coq_Saddo bs1 bs2)
                (coq_Saddo (addB bs1 bs2)
-                 (zext (subn a_size (Pervasives.succ 0)) c))
+                 (zext (subn a_size (Stdlib.succ 0)) c))
           then QFBV.QFBV.qfbv_false
           else QFBV.QFBV.qfbv_true))
 
@@ -596,7 +596,7 @@ let bexp_atom_usbbB_algsnd a_size a1 a2 ab =
     (QFBV.QFBV.qfbv_lneg
       (QFBV.QFBV.qfbv_usubo
         (QFBV.QFBV.qfbv_sub (qfbv_atom a1) (qfbv_atom a2))
-        (QFBV.QFBV.qfbv_zext (subn a_size (Pervasives.succ 0)) (qfbv_atom ab))))
+        (QFBV.QFBV.qfbv_zext (subn a_size (Stdlib.succ 0)) (qfbv_atom ab))))
 
 (** val bexp_atom_ssbbB_algsnd :
     int -> atom -> atom -> atom -> QFBV.QFBV.bexp **)
@@ -607,7 +607,7 @@ let bexp_atom_ssbbB_algsnd a_size a1 a2 ab =
     (QFBV.QFBV.qfbv_lneg
       (QFBV.QFBV.qfbv_ssubo
         (QFBV.QFBV.qfbv_sub (qfbv_atom a1) (qfbv_atom a2))
-        (QFBV.QFBV.qfbv_zext (subn a_size (Pervasives.succ 0)) (qfbv_atom ab))))
+        (QFBV.QFBV.qfbv_zext (subn a_size (Stdlib.succ 0)) (qfbv_atom ab))))
 
 (** val bexp_atom_sbbB_algsnd :
     TypEnv.SSATE.env -> SSALite.SSALite.atom -> atom -> atom -> QFBV.QFBV.bexp **)
@@ -638,8 +638,8 @@ let bexp_atom_usbcB_algsnd a_size a1 a2 ac =
     (QFBV.QFBV.qfbv_lneg
       (QFBV.QFBV.qfbv_usubo
         (QFBV.QFBV.qfbv_sub (qfbv_atom a1) (qfbv_atom a2))
-        (QFBV.QFBV.qfbv_zext (subn a_size (Pervasives.succ 0))
-          (QFBV.QFBV.qfbv_sub (QFBV.QFBV.qfbv_one (Pervasives.succ 0))
+        (QFBV.QFBV.qfbv_zext (subn a_size (Stdlib.succ 0))
+          (QFBV.QFBV.qfbv_sub (QFBV.QFBV.qfbv_one (Stdlib.succ 0))
             (qfbv_atom ac)))))
 
 (** val bexp_atom_ssbcB_algsnd :
@@ -651,8 +651,8 @@ let bexp_atom_ssbcB_algsnd a_size a1 a2 ac =
     (QFBV.QFBV.qfbv_lneg
       (QFBV.QFBV.qfbv_ssubo
         (QFBV.QFBV.qfbv_sub (qfbv_atom a1) (qfbv_atom a2))
-        (QFBV.QFBV.qfbv_zext (subn a_size (Pervasives.succ 0))
-          (QFBV.QFBV.qfbv_sub (QFBV.QFBV.qfbv_one (Pervasives.succ 0))
+        (QFBV.QFBV.qfbv_zext (subn a_size (Stdlib.succ 0))
+          (QFBV.QFBV.qfbv_sub (QFBV.QFBV.qfbv_one (Stdlib.succ 0))
             (qfbv_atom ac)))))
 
 (** val bexp_atom_sbcB_algsnd :
@@ -694,12 +694,12 @@ let bexp_atom_shl_algsnd e a n =
          (QFBV.QFBV.qfbv_zero n)
   else QFBV.QFBV.qfbv_disj
          (QFBV.QFBV.qfbv_eq
-           (QFBV.QFBV.qfbv_high (addn n (Pervasives.succ 0)) (qfbv_atom a))
-           (QFBV.QFBV.qfbv_zero (addn n (Pervasives.succ 0))))
+           (QFBV.QFBV.qfbv_high (addn n (Stdlib.succ 0)) (qfbv_atom a))
+           (QFBV.QFBV.qfbv_zero (addn n (Stdlib.succ 0))))
          (QFBV.QFBV.qfbv_eq
-           (QFBV.QFBV.qfbv_high (addn n (Pervasives.succ 0)) (qfbv_atom a))
+           (QFBV.QFBV.qfbv_high (addn n (Stdlib.succ 0)) (qfbv_atom a))
            (QFBV.QFBV.qfbv_not
-             (QFBV.QFBV.qfbv_zero (addn n (Pervasives.succ 0)))))
+             (QFBV.QFBV.qfbv_zero (addn n (Stdlib.succ 0)))))
 
 (** val bexp_atom_cshl_algsnd :
     TypEnv.SSATE.env -> SSALite.SSALite.atom -> atom -> int -> QFBV.QFBV.bexp **)
@@ -712,14 +712,14 @@ let bexp_atom_cshl_algsnd e a1 a2 n =
          (QFBV.QFBV.qfbv_zero n)
   else QFBV.QFBV.qfbv_disj
          (QFBV.QFBV.qfbv_eq
-           (QFBV.QFBV.qfbv_high (addn n (Pervasives.succ 0))
+           (QFBV.QFBV.qfbv_high (addn n (Stdlib.succ 0))
              (QFBV.QFBV.qfbv_concat (qfbv_atom a1) (qfbv_atom a2)))
-           (QFBV.QFBV.qfbv_zero (addn n (Pervasives.succ 0))))
+           (QFBV.QFBV.qfbv_zero (addn n (Stdlib.succ 0))))
          (QFBV.QFBV.qfbv_eq
-           (QFBV.QFBV.qfbv_high (addn n (Pervasives.succ 0))
+           (QFBV.QFBV.qfbv_high (addn n (Stdlib.succ 0))
              (QFBV.QFBV.qfbv_concat (qfbv_atom a1) (qfbv_atom a2)))
            (QFBV.QFBV.qfbv_not
-             (QFBV.QFBV.qfbv_zero (addn n (Pervasives.succ 0)))))
+             (QFBV.QFBV.qfbv_zero (addn n (Stdlib.succ 0)))))
 
 (** val bexp_atom_vpc_algsnd :
     TypEnv.SSATE.env -> typ -> SSALite.SSALite.atom -> QFBV.QFBV.bexp **)
@@ -736,25 +736,25 @@ let bexp_atom_vpc_algsnd e t a =
                    (QFBV.QFBV.qfbv_zero
                      (subn (sizeof_typ (SSALite.SSALite.atyp a e))
                        (sizeof_typ t)))
-       else if leq (Pervasives.succ (sizeof_typ (SSALite.SSALite.atyp a e)))
+       else if leq (Stdlib.succ (sizeof_typ (SSALite.SSALite.atyp a e)))
                  (sizeof_typ t)
             then QFBV.QFBV.qfbv_true
             else QFBV.QFBV.qfbv_eq
                    (QFBV.QFBV.qfbv_high
                      (addn
                        (subn (sizeof_typ (SSALite.SSALite.atyp a e))
-                         (sizeof_typ t)) (Pervasives.succ 0)) (qfbv_atom a))
+                         (sizeof_typ t)) (Stdlib.succ 0)) (qfbv_atom a))
                    (QFBV.QFBV.qfbv_zero
                      (addn
                        (subn (sizeof_typ (SSALite.SSALite.atyp a e))
-                         (sizeof_typ t)) (Pervasives.succ 0)))
+                         (sizeof_typ t)) (Stdlib.succ 0)))
   else if is_unsigned t
        then if leq
                  (subn (sizeof_typ (SSALite.SSALite.atyp a e))
-                   (Pervasives.succ 0)) (sizeof_typ t)
+                   (Stdlib.succ 0)) (sizeof_typ t)
             then QFBV.QFBV.qfbv_eq
-                   (QFBV.QFBV.qfbv_high (Pervasives.succ 0) (qfbv_atom a))
-                   (QFBV.QFBV.qfbv_zero (Pervasives.succ 0))
+                   (QFBV.QFBV.qfbv_high (Stdlib.succ 0) (qfbv_atom a))
+                   (QFBV.QFBV.qfbv_zero (Stdlib.succ 0))
             else QFBV.QFBV.qfbv_eq
                    (QFBV.QFBV.qfbv_high
                      (subn (sizeof_typ (SSALite.SSALite.atyp a e))
diff --git a/src/ocaml/extraction/SSA2REP.ml b/src/ocaml/extraction/SSA2REP.ml
index 16a46dd..b17af20 100644
--- a/src/ocaml/extraction/SSA2REP.ml
+++ b/src/ocaml/extraction/SSA2REP.ml
@@ -78,7 +78,7 @@ let algred_cast avn g v vtyp a atyp0 =
   | Tsint wv ->
     (match atyp0 with
      | Tuint wa ->
-       if leq (Pervasives.succ wa) wv
+       if leq (Stdlib.succ wa) wv
        then (g, ((Eeq ((SSALite.SSALite.evar v), (algred_atom a))) :: []))
        else let discarded = (avn, g) in
             let g' = N.succ g in
diff --git a/src/ocaml/extraction/State.ml b/src/ocaml/extraction/State.ml
index 378a2b6..112e8ef 100644
--- a/src/ocaml/extraction/State.ml
+++ b/src/ocaml/extraction/State.ml
@@ -110,7 +110,7 @@ module MakeBitsStore =
         let rec cardinal = function
         | Leaf -> 0
         | Node (l, _, _, r, _) ->
-          Pervasives.succ (add (cardinal l) (cardinal r))
+          Stdlib.succ (add (cardinal l) (cardinal r))
 
         (** val empty : 'a1 tree **)
 
diff --git a/src/ocaml/extraction/Typ.ml b/src/ocaml/extraction/Typ.ml
index 0a95680..43b9e76 100644
--- a/src/ocaml/extraction/Typ.ml
+++ b/src/ocaml/extraction/Typ.ml
@@ -47,7 +47,7 @@ let typ_eqType =
 (** val coq_Tbit : typ **)
 
 let coq_Tbit =
-  Tuint (Pervasives.succ 0)
+  Tuint (Stdlib.succ 0)
 
 (** val is_unsigned : typ -> bool **)
 
@@ -64,8 +64,8 @@ let unsigned_typ = function
 (** val double_typ : typ -> typ **)
 
 let double_typ = function
-| Tuint w -> Tuint (muln (Pervasives.succ (Pervasives.succ 0)) w)
-| Tsint w -> Tsint (muln (Pervasives.succ (Pervasives.succ 0)) w)
+| Tuint w -> Tuint (muln (Stdlib.succ (Stdlib.succ 0)) w)
+| Tsint w -> Tsint (muln (Stdlib.succ (Stdlib.succ 0)) w)
 
 (** val compatible : typ -> typ -> bool **)
 
diff --git a/src/ocaml/extraction/seq.ml b/src/ocaml/extraction/seq.ml
index d6a65c8..3f9882e 100644
--- a/src/ocaml/extraction/seq.ml
+++ b/src/ocaml/extraction/seq.ml
@@ -12,7 +12,7 @@ let __ = let rec f _ = Obj.repr f in Obj.repr f
 
 let rec size = function
 | [] -> 0
-| _ :: s' -> Pervasives.succ (size s')
+| _ :: s' -> Stdlib.succ (size s')
 
 (** val head : 'a1 -> 'a1 list -> 'a1 **)
 
diff --git a/src/ocaml/extraction/ssrnat.ml b/src/ocaml/extraction/ssrnat.ml
index c523b92..5c31ae9 100644
--- a/src/ocaml/extraction/ssrnat.ml
+++ b/src/ocaml/extraction/ssrnat.ml
@@ -64,12 +64,12 @@ let leq m n =
 (** val maxn : int -> int -> int **)
 
 let maxn m n =
-  if leq (Pervasives.succ m) n then n else m
+  if leq (Stdlib.succ m) n then n else m
 
 (** val minn : int -> int -> int **)
 
 let minn m n =
-  if leq (Pervasives.succ m) n then m else n
+  if leq (Stdlib.succ m) n then m else n
 
 (** val iter : int -> ('a1 -> 'a1) -> 'a1 -> 'a1 **)
 
@@ -92,7 +92,7 @@ let muln =
 (** val nat_of_bool : bool -> int **)
 
 let nat_of_bool = function
-| true -> Pervasives.succ 0
+| true -> Stdlib.succ 0
 | false -> 0
 
 (** val odd : int -> bool **)
@@ -108,7 +108,7 @@ let rec odd n =
 let rec double_rec n =
   (fun fO fS n -> if n=0 then fO () else fS (n-1))
     (fun _ -> 0)
-    (fun n' -> Pervasives.succ (Pervasives.succ (double_rec n')))
+    (fun n' -> Stdlib.succ (Stdlib.succ (double_rec n')))
     n
 
 (** val double : int -> int **)
@@ -129,7 +129,7 @@ let rec half n =
 and uphalf n =
   (fun fO fS n -> if n=0 then fO () else fS (n-1))
     (fun _ -> n)
-    (fun n' -> Pervasives.succ (half n'))
+    (fun n' -> Stdlib.succ (half n'))
     n
 
 (** val eq_binP : coq_N Equality.axiom **)