From a3b4f4dceccff607274a7c28cc134c4377e2956f Mon Sep 17 00:00:00 2001 From: Karolis Petrauskas Date: Wed, 31 Jan 2024 22:20:53 +0200 Subject: [PATCH] Make it compile on OCaml 5.1. Signed-off-by: Karolis Petrauskas --- src/backend/smtlib.ml | 2 +- src/encode/n_axiomatize.ml | 2 +- src/encode/n_flatten.ml | 2 +- src/encode/n_rewrite.ml | 2 +- src/encode/n_smb.ml | 2 +- src/expr/e_elab.ml | 2 +- src/util/property.mli | 2 +- tools/newversion.ml | 2 +- 8 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/backend/smtlib.ml b/src/backend/smtlib.ml index 21b717aa..6adf4358 100644 --- a/src/backend/smtlib.ml +++ b/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 diff --git a/src/encode/n_axiomatize.ml b/src/encode/n_axiomatize.ml index b3902c4a..702bb38f 100644 --- a/src/encode/n_axiomatize.ml +++ b/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 diff --git a/src/encode/n_flatten.ml b/src/encode/n_flatten.ml index 4e132c10..54071fc8 100644 --- a/src/encode/n_flatten.ml +++ b/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 = diff --git a/src/encode/n_rewrite.ml b/src/encode/n_rewrite.ml index 4cfeea06..53c3a5d4 100644 --- a/src/encode/n_rewrite.ml +++ b/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 diff --git a/src/encode/n_smb.ml b/src/encode/n_smb.ml index 2fb25ff0..4e096b85 100644 --- a/src/encode/n_smb.ml +++ b/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) diff --git a/src/expr/e_elab.ml b/src/expr/e_elab.ml index 13a42bc4..798f6d3a 100644 --- a/src/expr/e_elab.ml +++ b/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)) *) diff --git a/src/util/property.mli b/src/util/property.mli index 57d63b7e..8973d0a5 100644 --- a/src/util/property.mli +++ b/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 diff --git a/tools/newversion.ml b/tools/newversion.ml index 8973d03b..47b21d9c 100644 --- a/tools/newversion.ml +++ b/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%!" ;;