diff --git a/src/bin/common/input_frontend.ml b/src/bin/common/input_frontend.ml
index de8246413..d12d25790 100644
--- a/src/bin/common/input_frontend.ml
+++ b/src/bin/common/input_frontend.ml
@@ -42,11 +42,11 @@ let register_legacy () =
 
     let parse_file ~content ~format =
       let l = Parsers.parse_problem_as_string ~content ~format in
-      Lists.to_seq l
+      Stdcompat.List.to_seq l
 
     let parse_files ~filename ~preludes =
       let l = Parsers.parse_problem ~filename ~preludes in
-      Lists.to_seq l
+      Stdcompat.List.to_seq l
 
     (* Typechecking *)
 
diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml
index c764ef18e..3e5d5cb9c 100644
--- a/src/bin/common/parse_command.ml
+++ b/src/bin/common/parse_command.ml
@@ -662,13 +662,13 @@ let parse_execution_opt =
       else
         match Config.lookup_prelude p with
         | Some p' ->
-          begin if Compat.String.starts_with ~prefix:"b-set-theory" p then
+          begin if Stdcompat.String.starts_with ~prefix:"b-set-theory" p then
               Printer.print_wrn ~header:true
                 "Support for the B set theory is deprecated since version \
                  2.5.0 and may be removed in a future version. If you are \
                  actively using it, please make yourself known to the Alt-Ergo \
                  developers by writing to <alt-ergo@ocamlpro.com>."
-            else if Compat.String.starts_with ~prefix:"fpa-theory" p then
+            else if Stdcompat.String.starts_with ~prefix:"fpa-theory" p then
               Printer.print_wrn ~header:true
                 "@[Support for the FPA theory has been integrated as a builtin \
                  theory prelude in version 2.5.0. Please use \
diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml
index 327ed9208..9c9b0b032 100644
--- a/src/bin/common/solving_loop.ml
+++ b/src/bin/common/solving_loop.ml
@@ -219,7 +219,7 @@ let main () =
                 ~format:(Some (Filename.extension filename)))
         in
         let preludes = Options.get_preludes () in
-        Compat.Seq.append theory_preludes @@
+        Stdcompat.Seq.append theory_preludes @@
         I.parse_files ~filename ~preludes
       with
       | Util.Timeout ->
diff --git a/src/lib/dune b/src/lib/dune
index af2e9e726..ef5d8311a 100644
--- a/src/lib/dune
+++ b/src/lib/dune
@@ -50,7 +50,7 @@
     Emap Gc_debug Hconsing Hstring Iheap Lists Loc
     MyUnix Numbers
     Options Timers Util Vec Version Steps Printer My_zip
-    Theories Compat
+    Theories
   )
 
  (js_of_ocaml
diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml
index 43c2fbc05..97bd1bc34 100644
--- a/src/lib/reasoners/bitv.ml
+++ b/src/lib/reasoners/bitv.ml
@@ -130,7 +130,7 @@ let int2bv_const n z =
   done;
   !acc
 
-let equal_abstract eq = Lists.equal (equal_simple_term eq)
+let equal_abstract eq = Stdcompat.List.equal (equal_simple_term eq)
 
 (* for the solver *)
 
@@ -200,7 +200,7 @@ module Shostak(X : ALIEN) = struct
           if c2 <> 0 then c2 else X.str_cmp t1 t2
     )
 
-  let compare_abstract = Lists.compare compare_simple_term
+  let compare_abstract = Stdcompat.List.compare compare_simple_term
 
   (* Compare two simple terms. The [equalities_propagation] function below
      requires that : [false ≤ st ≤ true] for all simple terms [st]. *)
@@ -977,9 +977,9 @@ module Shostak(X : ALIEN) = struct
               let _fw = apply_subs subs r in
               let eq (_, l1) (_, l2) =
                 (* [apply_subs] does not change the left-hand sides *)
-                Lists.equal (Lists.equal equal_solver_simple_term) l1 l2
+                Stdcompat.List.(equal (equal equal_solver_simple_term) l1 l2)
               in
-              if Lists.equal eq _bw bw
+              if Stdcompat.List.equal eq _bw bw
               then slice_rec ((t,vls')::bw) _fw
               else slice_rec [] (_bw@((t,vls'):: _fw))
             end
diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml
index 6cdb5e6fb..65290d0a8 100644
--- a/src/lib/reasoners/satml.ml
+++ b/src/lib/reasoners/satml.ml
@@ -756,7 +756,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
             List.fold_left (add_aux env) ma l
 
           | OR l  ->
-            match Lists.find_opt (fun e ->
+            match Stdcompat.List.find_opt (fun e ->
                 let p = get_atom_or_proxy e env.proxies in
                 p.is_true) l
             with
diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml
index 1045389f6..5b886b63a 100644
--- a/src/lib/structures/symbols.ml
+++ b/src/lib/structures/symbols.ml
@@ -107,7 +107,7 @@ let var s = Var s
 let int i = Int (Z.of_string i)
 let bitv s =
   let biv =
-    Compat.String.fold_left (fun n c ->
+    Stdcompat.String.fold_left (fun n c ->
         match c with
         | '0' -> Z.(n lsl 1)
         | '1' -> Z.((n lsl 1) lor ~$1)
@@ -135,8 +135,8 @@ let is_internal sy =
   match sy with
   | Name (hs, _, _) ->
     let s = Hstring.view hs in
-    Compat.String.starts_with ~prefix:"." s ||
-    Compat.String.starts_with ~prefix:"@" s
+    Stdcompat.String.starts_with ~prefix:"." s ||
+    Stdcompat.String.starts_with ~prefix:"@" s
   | _ -> false
 
 let underscore =
diff --git a/src/lib/util/compat.ml b/src/lib/util/compat.ml
deleted file mode 100644
index 2d5242211..000000000
--- a/src/lib/util/compat.ml
+++ /dev/null
@@ -1,25 +0,0 @@
-module String = struct
-  open Stdlib.String
-
-  let starts_with ~prefix s =
-    length s >= length prefix &&
-    equal (sub s 0 (length prefix)) prefix
-
-  let fold_left f x a =
-    let r = ref x in
-    for i = 0 to length a - 1 do
-      r := f !r (unsafe_get a i)
-    done;
-    !r
-end
-
-module Seq = struct
-  type 'a t = 'a Stdlib.Seq.t
-
-  open Stdlib.Seq
-
-  let rec append xs ys () =
-    match xs () with
-    | Nil -> ys ()
-    | Cons (x, xs) -> Cons (x, append xs ys)
-end
diff --git a/src/lib/util/compat.mli b/src/lib/util/compat.mli
deleted file mode 100644
index d5a54e65c..000000000
--- a/src/lib/util/compat.mli
+++ /dev/null
@@ -1,47 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     Alt-Ergo: The SMT Solver For Software Verification                 *)
-(*     Copyright (C) 2013-2023 --- OCamlPro SAS                           *)
-(*                                                                        *)
-(*     This file is distributed under the terms of OCamlPro               *)
-(*     Non-Commercial Purpose License, version 1.                         *)
-(*                                                                        *)
-(*     As an exception, Alt-Ergo Club members at the Gold level can       *)
-(*     use this file under the terms of the Apache Software License       *)
-(*     version 2.0.                                                       *)
-(*                                                                        *)
-(*     ---------------------------------------------------------------    *)
-(*                                                                        *)
-(*     The Alt-Ergo theorem prover                                        *)
-(*                                                                        *)
-(*     Sylvain Conchon, Evelyne Contejean, Francois Bobot                 *)
-(*     Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout              *)
-(*                                                                        *)
-(*     CNRS - INRIA - Universite Paris Sud                                *)
-(*                                                                        *)
-(*     Until 2013, some parts of this code were released under            *)
-(*     the Apache Software License version 2.0.                           *)
-(*                                                                        *)
-(*     ---------------------------------------------------------------    *)
-(*                                                                        *)
-(*     More details can be found in the directory licenses/               *)
-(*                                                                        *)
-(**************************************************************************)
-
-(** This module enables some of the newer functions from OCaml's stdlib while
-    still supporting old versions of the compiler. *)
-
-module String : sig
-  (* @since 4.13.0 *)
-  val starts_with : prefix:string -> string -> bool
-
-  (* @since 4.13.0 *)
-  val fold_left : ('acc -> char -> 'acc) -> 'acc -> string -> 'acc
-end
-
-module Seq : sig
-  type 'a t = 'a Stdlib.Seq.t
-
-  (* @since 4.11.0 *)
-  val append : 'a t -> 'a t -> 'a t
-end
diff --git a/src/lib/util/lists.ml b/src/lib/util/lists.ml
index 26c6d6233..f959ac1a1 100644
--- a/src/lib/util/lists.ml
+++ b/src/lib/util/lists.ml
@@ -51,36 +51,3 @@ let apply_right f l =
       )([], true) l
   in
   (if same then l else List.rev res), same
-
-let rec find_opt pred l =
-  match l with
-  | [] -> None
-  | e :: r ->
-    if pred e then Some e
-    else find_opt pred r
-
-let to_seq l =
-  let rec aux l () = match l with
-    | [] -> Seq.Nil
-    | x :: tail -> Seq.Cons (x, aux tail)
-  in
-  aux l
-
-(* TODO: This function is supported by the Stdlib from OCaml 4.12. *)
-let rec compare cmp l1 l2 =
-  match l1, l2 with
-  | [], [] -> 0
-  | [], _ -> -1
-  | _, [] -> 1
-  | hd1::tl1, hd2::tl2 ->
-    let c = cmp hd1 hd2 in
-    if c <> 0 then c
-    else
-      compare cmp tl1 tl2
-
-(* List.equal in OCaml 4.12+ *)
-let rec equal eq l1 l2 =
-  match l1, l2 with
-  | [], [] -> true
-  | hd1 :: tl1, hd2 :: tl2 when eq hd1 hd2 -> equal eq tl1 tl2
-  | _ -> false
diff --git a/src/lib/util/lists.mli b/src/lib/util/lists.mli
index 684f0ca23..01cb2555b 100644
--- a/src/lib/util/lists.mli
+++ b/src/lib/util/lists.mli
@@ -38,9 +38,6 @@
 val is_empty : 'a list -> bool
 (** Is the list empty? *)
 
-val to_seq : 'a list -> 'a Seq.t
-(** Iterate on the list *)
-
 val apply : ('a -> 'a) -> 'a list -> 'a list * bool
 (** [apply f [a_1; ...; a_n]] returns a couple [[f a_1; ...; f a_n], same]
     same such that: (1) "same" is true if and only if a_i == a_i for
@@ -50,17 +47,3 @@ val apply : ('a -> 'a) -> 'a list -> 'a list * bool
 val apply_right : ('a -> 'a) -> ('b * 'a) list -> ('b * 'a) list * bool
 (** similar to function apply, but the elements of the list are
     couples **)
-
-val find_opt : ('a -> bool) -> 'a list -> 'a option
-(** Tries and find the first element of the list satisfying the predicate. *)
-
-val compare : ('a -> 'a -> int) -> 'a list -> 'a list -> int
-(** [compare cmp l1 l2] compares the lists [l1] and [l2] using the comparison
-    function [cmp] on elements. *)
-
-val equal : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool
-(** [equal eq l1 l2] holds when the two input lists have the same length and for
-    each pair of elements [ai], [bi] at the same position in [l1] and [l2]
-    respectively, we have [eq ai bi].
-
-    This is a backport of List.equal from OCaml 4.12.0 *)