Make it compile on OCaml 5.1.

src/backend/smtlib.ml

@@ -20,7 +20,7 @@ module Smb = Encode.Smb
 module T = Encode.Table
 module B = Builtin
 
-let (@@@) = Pervasives.(@@)
+let (@@@) = Stdlib.(@@)
 
 let error ?at mssg =
   let mssg = "Backend.Smtlib: " ^ mssg in

src/encode/n_axiomatize.ml

@@ -19,7 +19,7 @@ open N_table
 
 module TlaAxmSet = Set.Make (struct
   type t = tla_axm
-  let compare = Pervasives.compare
+  let compare = Stdlib.compare
 end)
 
 type ecx = s * SmbSet.t * TlaAxmSet.t

src/encode/n_flatten.ml

@@ -239,7 +239,7 @@ let find_hoapp_visitor = object (self : 'self)
                 Is.union vs vs_e
               end Is.empty ho_args |>
               Is.elements |>
-              List.sort ~cmp:(fun i j -> Pervasives.compare j i)
+              List.sort ~cmp:(fun i j -> Stdlib.compare j i)
             in
 
             let bp =

src/encode/n_rewrite.ml

@@ -539,7 +539,7 @@ let elim_records sq =
 (* {3 Sort Record Fields} *)
 
 let cmp_fs (f1, e1) (f2, e2) =
-  Pervasives.compare f1 f2
+  Stdlib.compare f1 f2
 
 let sort_recfields_visitor = object (self : 'self)
   inherit [unit] Expr.Visit.map as super

src/encode/n_smb.ml

@@ -30,7 +30,7 @@ let smb_prop = make "Encode.Smb.smb_prop"
 module SmbOrd = struct
   type t = smb
   let compare smb1 smb2 =
-    Pervasives.compare smb1.smb_name smb2.smb_name
+    Stdlib.compare smb1.smb_name smb2.smb_name
 end
 
 module SmbSet = Set.Make (SmbOrd)

src/expr/e_elab.ml

@@ -277,7 +277,7 @@ let%test_module _ = (module struct
     let test_case = create_expression test_string in
     let target_case = create_expression "f'[x']" in
     (* let x = normalize Deque.empty test_case in
-       Printf.eprintf "compare: %d\n" (Pervasives.compare x target_case); *)
+       Printf.eprintf "compare: %d\n" (Stdlib.compare x target_case); *)
       [%test_eq: string] (prn_exp target_case) (prn_exp (normalize Deque.empty test_case))
   *)
 

src/util/property.mli

@@ -19,7 +19,7 @@
 *)
 
 (** Property identifiers. They may be safely compared using
-    [Pervasives.compare]. *)
+    [Stdlib.compare]. *)
 type pid
 
 (** The abstract type of "properties". All types can be injected and

tools/newversion.ml

@@ -105,6 +105,6 @@ let () =
   let ret = Sys.command ("autoconf -I tools -o configure " ^ acf) in
   if ret <> 0 then failwith "calling autoconf" ;
   if !loud then printf "Created configure\n%!" ;
-  flush Pervasives.stdout ;
+  flush Stdlib.stdout ;
   if !loud then printf "Now run ./configure to rebuild the Makefile\n%!"
 ;;