Upgrade to OCaml 5.3

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

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 **)

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

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)))

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

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

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

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

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

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 **)
 

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)))

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 =

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

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 **)
 

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)

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 **)

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