diff --git a/CHANGES.md b/CHANGES.md
index fb004fb7b..b7e1f926a 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -91,7 +91,6 @@
    `(alt-ergo plugins)` site to be picked up by Alt-Ergo (#1049).
  - Add a release workflow (#827)
  - Mark the dune.inc file as linguist-generated to avoid huge diffs (#830)
- - Use stdcompat to support older OCaml versions (#866)
  - Use GitHub Actions badges in the README (#882)
  - Use `dune build @check` to build the project (#887)
  - Enable warnings as errors on the CI (#888)
diff --git a/alt-ergo-lib.opam b/alt-ergo-lib.opam
index db14b3552..0e6615c84 100644
--- a/alt-ergo-lib.opam
+++ b/alt-ergo-lib.opam
@@ -30,7 +30,6 @@ depends: [
   "camlzip" {>= "1.07"}
   "odoc" {with-doc}
   "ppx_deriving"
-  "stdcompat"
   "qcheck" {with-test}
 ]
 conflicts: [
diff --git a/alt-ergo-lib.opam.locked b/alt-ergo-lib.opam.locked
index 56c8ae728..d3c041919 100644
--- a/alt-ergo-lib.opam.locked
+++ b/alt-ergo-lib.opam.locked
@@ -57,7 +57,6 @@ depends: [
   "seq" {= "base"}
   "sexplib0" {= "v0.16.0"}
   "spelll" {= "0.4"}
-  "stdcompat" {= "19"}
   "topkg" {= "1.0.7"}
   "uutf" {= "1.0.3"}
   "yojson" {= "2.1.1"}
diff --git a/default.nix b/default.nix
index b0d4b045e..b8cc07982 100644
--- a/default.nix
+++ b/default.nix
@@ -24,7 +24,6 @@ let
       dolmen_loop
       camlzip
       ppx_deriving
-      stdcompat
     ];
   };
 
diff --git a/dune-project b/dune-project
index 8cac728ce..45da9e850 100644
--- a/dune-project
+++ b/dune-project
@@ -90,7 +90,6 @@ See more details on http://alt-ergo.ocamlpro.com/"
   (camlzip (>= 1.07))
   (odoc :with-doc)
   ppx_deriving
-  stdcompat
   (qcheck :with-test)
  )
  (conflicts
diff --git a/shell.nix b/shell.nix
index b4438ffb3..e236f54d6 100644
--- a/shell.nix
+++ b/shell.nix
@@ -40,7 +40,6 @@ pkgs.mkShell {
     ppx_blob
     odoc
     ppx_deriving
-    stdcompat
     landmarks
     landmarks-ppx
     qcheck
diff --git a/src/bin/common/input_frontend.ml b/src/bin/common/input_frontend.ml
index 93a498290..16c7ce72b 100644
--- a/src/bin/common/input_frontend.ml
+++ b/src/bin/common/input_frontend.ml
@@ -39,11 +39,11 @@ let register_legacy () =
 
     let parse_file ~content ~format =
       let l = Parsers.parse_problem_as_string ~content ~format in
-      Stdcompat.List.to_seq l
+      List.to_seq l
 
     let parse_files ~filename ~preludes =
       let l = Parsers.parse_problem ~filename ~preludes in
-      Stdcompat.List.to_seq l
+      List.to_seq l
 
     (* Typechecking *)
 
diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml
index 964b9dc76..6085fd342 100644
--- a/src/bin/common/parse_command.ml
+++ b/src/bin/common/parse_command.ml
@@ -69,7 +69,7 @@ let formats_list =
 
 let format_parser s =
   try
-    Ok (Lists.assoc String.equal s formats_list)
+    Ok (My_list.assoc String.equal s formats_list)
   with
     Not_found ->
     Error (`Msg (Format.sprintf
@@ -462,13 +462,14 @@ let mk_theory_opt () no_contracongru
     no_fm no_nla no_tcp no_theory restricted tighten_vars
     _use_fpa (theories)
   =
-  set_no_ac (not (Lists.mem Theories.equal Theories.AC theories));
+  set_no_ac (not (List.exists (Theories.equal Theories.AC) theories));
   set_no_fm no_fm;
   set_no_nla no_nla;
   set_no_tcp no_tcp;
   set_no_theory no_theory;
   set_restricted restricted;
-  set_disable_adts (not (Lists.mem Theories.equal Theories.ADT theories));
+  set_disable_adts
+    (not (List.exists (Theories.equal Theories.ADT) theories));
   set_tighten_vars tighten_vars;
   set_no_contracongru no_contracongru;
   set_theory_preludes (Theories.preludes theories);
@@ -680,13 +681,13 @@ let parse_execution_opt =
       else
         match Config.lookup_prelude p with
         | Some p' ->
-          begin if Stdcompat.String.starts_with ~prefix:"b-set-theory" p then
+          begin if Compat.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 Stdcompat.String.starts_with ~prefix:"fpa-theory" p then
+            else if Compat.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 and is enabled \
@@ -1316,7 +1317,7 @@ let parse_theory_opt =
 
   let inequalities_plugin =
     let load_inequalities_plugin debug path =
-      let debug = List.exists (Lists.mem Debug.equal Debug.Fm) debug in
+      let debug = List.exists (List.exists (Debug.equal Debug.Fm)) debug in
       match path with
       | "" ->
         if debug then
diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml
index 80e4da051..8c14a00f5 100644
--- a/src/bin/common/solving_loop.ml
+++ b/src/bin/common/solving_loop.ml
@@ -278,7 +278,7 @@ let main () =
                 ~format:(Some (Filename.extension filename)))
         in
         let preludes = Options.get_preludes () in
-        Stdcompat.Seq.append theory_preludes @@
+        Compat.Seq.append theory_preludes @@
         I.parse_files ~filename ~preludes
       with
       | Util.Timeout ->
diff --git a/src/bin/text/dune b/src/bin/text/dune
index c913b5711..e41df7dcf 100644
--- a/src/bin/text/dune
+++ b/src/bin/text/dune
@@ -3,7 +3,7 @@
 
 (executable
   (name gen_link_flags)
-  (libraries unix fmt stdcompat)
+  (libraries unix fmt)
   (modules gen_link_flags))
 
 (rule
diff --git a/src/bin/text/gen_link_flags.ml b/src/bin/text/gen_link_flags.ml
index 97f7839b0..f44435a5a 100644
--- a/src/bin/text/gen_link_flags.ml
+++ b/src/bin/text/gen_link_flags.ml
@@ -5,12 +5,21 @@ let pkgconfig lib archive =
 
 let pp_lib ppf s = Fmt.pf ppf "-cclib %s" s
 
+let starts_with ~prefix s =
+  let open String in
+  let len_s = length s
+  and len_pre = length prefix in
+  let rec aux i =
+    if i = len_pre then true
+    else if unsafe_get s i <> unsafe_get prefix i then false
+    else aux (i + 1)
+  in len_s >= len_pre && aux 0
+
 let () =
   let mixed_flags = ["-noautolink"] in
   (* Note: for OCaml 5, use -lcamlstrnat and -lunixnat and mind zlib
      https://github.com/ocaml/ocaml/issues/12562 *)
   let mixed_cclib = [
-    "-lstdcompat_stubs";
     "-lcamlzip";
     "-lzarith";
     "-lcamlstr";
@@ -32,7 +41,7 @@ let () =
                   List.map
                     (fun lib ->
                        let archive =
-                         if Stdcompat.String.starts_with
+                         if starts_with
                              ~prefix:"lib" lib then
                            Fmt.str "%s.a" lib
                          else
diff --git a/src/lib/dune b/src/lib/dune
index 3f0c555f7..468d021a5 100644
--- a/src/lib/dune
+++ b/src/lib/dune
@@ -24,7 +24,6 @@
     dune-build-info
     alt_ergo_prelude
     fmt
-    stdcompat
   )
   (preprocess
     (pps
@@ -59,10 +58,9 @@
     Parsed Profiling Satml_types Symbols
     Expr Var Ty Typed Xliteral ModelMap Id Uid Objective Literal
     ; util
-    Emap Gc_debug Hconsing Hstring Heap Lists Loc
-    MyUnix Numbers Uqueue
-    Options Timers Util Vec Version Steps Printer My_zip
-    Theories Nest
+    Emap Gc_debug Hconsing Hstring Heap Loc Numbers Uqueue
+    Options Timers Util Vec Version Steps Printer
+    My_zip My_unix My_list Theories Nest Compat
   )
 
  (js_of_ocaml
diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml
index 76c0ec75f..7c417b946 100644
--- a/src/lib/frontend/d_cnf.ml
+++ b/src/lib/frontend/d_cnf.ml
@@ -1597,7 +1597,7 @@ and make_trigger ?(loc = Loc.dummy) ~name_base ~decl_kind
   (* clean trigger:
      remove useless terms in multi-triggers after inlining of lets*)
   let trigger = E.mk_trigger ~user:from_user ~hyp content in
-  if not in_theory && not (Lists.is_empty trigger.semantic) then
+  if not in_theory && not (Compat.List.is_empty trigger.semantic) then
     Errors.typing_error ThSemTriggerError loc;
   E.clean_trigger ~in_theory name trigger
 
diff --git a/src/lib/frontend/typechecker.ml b/src/lib/frontend/typechecker.ml
index afdf3c048..569b4f85d 100644
--- a/src/lib/frontend/typechecker.ml
+++ b/src/lib/frontend/typechecker.ml
@@ -142,7 +142,7 @@ module Types = struct
       let ty = Ty.text ty_vars (Uid.of_string id) in
       ty, { env with to_ty = MString.add id ty env.to_ty }
     | Enum l ->
-      if not (Lists.is_empty ty_vars) then
+      if not (Compat.List.is_empty ty_vars) then
         Errors.typing_error (PolymorphicEnum id) loc;
       let body = List.map (fun constr -> Uid.of_string constr, []) l in
       let ty = Ty.t_adt ~body:(Some body) (Uid.of_string id) [] in
@@ -202,7 +202,7 @@ module Types = struct
         Errors.typing_error WrongNumberOfLabels loc;
       List.iter
         (fun (lb, _) ->
-           try ignore (Lists.assoc Uid.equal lb l)
+           try ignore (My_list.assoc Uid.equal lb l)
            with Not_found ->
              Errors.typing_error
                (WrongLabel((Hstring.make @@ Uid.show lb), ty)) loc) lbs;
@@ -869,7 +869,7 @@ let rec type_term ?(call_from_type_form=false) env f =
           begin
             try
               TTdot(te, Hstring.make a),
-              Lists.assoc Uid.equal (Uid.of_string a) lbs
+              My_list.assoc Uid.equal (Uid.of_string a) lbs
             with Not_found ->
               let g = Uid.show g in
               Errors.typing_error (ShouldHaveLabel(g,a)) t.pp_loc
diff --git a/src/lib/index.mld b/src/lib/index.mld
index 30345cfd4..912d4d5a9 100644
--- a/src/lib/index.mld
+++ b/src/lib/index.mld
@@ -148,13 +148,14 @@ AltErgoLib.Util
 AltErgoLib.Heap
 AltErgoLib.Emap
 AltErgoLib.Hstring
-AltErgoLib.Lists
+AltErgoLib.Compat
 AltErgoLib.Gc_debug
 AltErgoLib.Timers
 AltErgoLib.Hconsing
 AltErgoLib.Vec
 AltErgoLib.Loc
-AltErgoLib.MyUnix
+AltErgoLib.My_unix
+AltErgoLib.My_list
 AltErgoLib.Numbers
 }
 
diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml
index 3d0522fc3..3c1dafd98 100644
--- a/src/lib/reasoners/adt.ml
+++ b/src/lib/reasoners/adt.ml
@@ -416,7 +416,9 @@ module Shostak (X : ALIEN) = struct
   let to_model_term r =
     match embed r with
     | Constr { c_name; c_ty; c_args } ->
-      let args = Lists.try_map (fun (_, arg) -> X.to_model_term arg) c_args in
+      let args =
+        My_list.try_map (fun (_, arg) -> X.to_model_term arg) c_args
+      in
       Option.bind args @@ fun args ->
       Some (E.mk_constr c_name args c_ty)
 
diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml
index 6355fd1a0..f0f45ccd3 100644
--- a/src/lib/reasoners/adt_rel.ml
+++ b/src/lib/reasoners/adt_rel.ml
@@ -177,7 +177,7 @@ module Domains = struct
     match X.type_info r with
     | Tadt (name, args) ->
       let cases = Ty.type_body name args in
-      Lists.is_empty @@ Ty.assoc_destrs c cases
+      Compat.List.is_empty @@ Ty.assoc_destrs c cases
     | _ -> assert false
 
   let internal_update r nd t =
@@ -267,7 +267,7 @@ let calc_destructor d e uf =
   let r, ex = Uf.find uf e in
   match Th.embed r with
   | Constr { c_args; _ } ->
-    begin match Lists.assoc Uid.equal d c_args with
+    begin match My_list.assoc Uid.equal d c_args with
       | v -> Some (v, ex)
       | exception Not_found -> None
     end
@@ -511,7 +511,7 @@ let build_constr_eq r c =
            a nonempty context only for interpreted semantic values
            of the `Arith` and `Records` theories. The semantic
            values `cons` never involves such values. *)
-        assert (Lists.is_empty ctx);
+        assert (Compat.List.is_empty ctx);
         let eq = Shostak.L.(view @@ mk_eq r r') in
         Some (eq, E.mk_constr c xs ty)
 
@@ -674,7 +674,7 @@ let split_domain ~for_model env uf =
        a nonempty context only for interpreted semantic values
        of the `Arith` and `Records` theories. The semantic
        values `cons` never involves such values. *)
-    assert (Lists.is_empty ctx);
+    assert (Compat.List.is_empty ctx);
     Some (LR.mkv_eq r nr)
   else
     None
diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml
index c877db96a..1c8fe5fb2 100644
--- a/src/lib/reasoners/bitv.ml
+++ b/src/lib/reasoners/bitv.ml
@@ -273,9 +273,9 @@ let to_Z_opt r = to_Z_opt_aux Z.zero r
 let int2bv_const n z =
   [ { bv = Cte (Z.extract z 0 n) ; sz = n } ]
 
-let equal_abstract eq = Stdcompat.List.equal (equal_simple_term eq)
+let equal_abstract eq = Compat.List.equal (equal_simple_term eq)
 
-let compare_abstract cmp = Stdcompat.List.compare (compare_simple_term cmp)
+let compare_abstract cmp = Compat.List.compare (compare_simple_term cmp)
 
 let hash_abstract hash =
   List.fold_left (fun acc e -> acc + 19 * hash_simple_term hash e) 19
@@ -557,7 +557,8 @@ module Shostak(X : ALIEN) = struct
 
     exception Valid
 
-    let add elt l = if Lists.mem (equal_signed X.equal) elt l then l else elt::l
+    let add elt l =
+      if List.exists (equal_signed X.equal elt) l then l else elt::l
 
     let get_vars = List.fold_left
         (fun ac st -> match st.bv with
@@ -601,8 +602,8 @@ module Shostak(X : ALIEN) = struct
       let f_add (s1,s2) acc =
         let b =
           equal_simple_term X.equal s1 s2
-          || Lists.mem equal_pair_simple_term (s1,s2) acc
-          || Lists.mem equal_pair_simple_term (s2,s1) acc
+          || List.exists (equal_pair_simple_term (s1,s2)) acc
+          || List.exists (equal_pair_simple_term (s2,s1)) acc
         in
         if b then acc else (s1,s2)::acc
       in let rec f_rec acc = function
@@ -1035,7 +1036,7 @@ module Shostak(X : ALIEN) = struct
            a B-variable has been split into parts below.
            Therefore we assert that the variable is indeed a B variable and that
            list of substitutions for B variables is not empty. *)
-        assert (not (Lists.is_empty (fst subs)));
+        assert (not (Compat.List.is_empty (fst subs)));
         assert (
           match st.bv.defn with Droot { sorte = B; _ } -> true | _ -> false
         );
@@ -1163,17 +1164,17 @@ module Shostak(X : ALIEN) = struct
         |[] -> bw
         |(t,vls)::r ->
           let (vls', csub) = uniforme_slice vls in
-          if Lists.is_empty csub then slice_rec ((t,vls')::bw) r
+          if Compat.List.is_empty csub then slice_rec ((t,vls')::bw) r
           else
             begin
               let _bw = apply_subs csub bw in
               let _fw = apply_subs csub r in
               let eq (_, l1) (_, l2) =
                 (* [apply_subs] does not change the left-hand sides *)
-                Stdcompat.List.(equal (equal (equal_alpha_term equal_tvar)))
+                Compat.List.(equal (equal (equal_alpha_term equal_tvar)))
                   l1 l2
               in
-              if Stdcompat.List.equal eq _bw bw
+              if Compat.List.equal eq _bw bw
               then slice_rec ((t,vls')::bw) _fw
               else slice_rec [] (_bw@((t,vls'):: _fw))
             end
@@ -1243,7 +1244,7 @@ module Shostak(X : ALIEN) = struct
       else begin
         let varsU = get_vars u in
         let varsV = get_vars v in
-        if Lists.is_empty varsU && Lists.is_empty varsV
+        if Compat.List.is_empty varsU && Compat.List.is_empty varsV
         then raise Util.Unsolvable
         else
           begin
@@ -1451,7 +1452,7 @@ module Shostak(X : ALIEN) = struct
       Printer.print_dbg
         ~module_name:"Bitv" ~function_name:"subst"
         "subst %a |-> %a in %a" X.print x X.print subs print biv;
-    if Lists.is_empty biv then is_mine biv
+    if Compat.List.is_empty biv then is_mine biv
     else
       let r = Canon.normalize (subst_rec x subs biv) in
       is_mine r
@@ -1484,7 +1485,7 @@ module Shostak(X : ALIEN) = struct
 
   let abstract_selectors v acc =
     let acc, v =
-      Stdcompat.List.fold_left_map (fun acc bv ->
+      Compat.List.fold_left_map (fun acc bv ->
           match bv with
           | { bv = Cte _ ; _ } -> acc, bv
           | { bv = Other { negated ; value = r } ; sz } ->
diff --git a/src/lib/reasoners/bitv_rel.ml b/src/lib/reasoners/bitv_rel.ml
index 866517318..a01da546b 100644
--- a/src/lib/reasoners/bitv_rel.ml
+++ b/src/lib/reasoners/bitv_rel.ml
@@ -1316,7 +1316,7 @@ let assume env uf la =
       let eqs, constraints, domain, int_domain =
         propagate_all eqs constraints domain int_domain
       in
-      if Options.get_debug_bitv () && not (Lists.is_empty eqs) then (
+      if Options.get_debug_bitv () && not (Compat.List.is_empty eqs) then (
         Printer.print_dbg
           ~module_name:"Bitv_rel" ~function_name:"assume"
           "bitlist domain: @[%a@]" Bitlist_domains.pp domain;
diff --git a/src/lib/reasoners/intervals.ml b/src/lib/reasoners/intervals.ml
index 243e1ca45..6e1296b38 100644
--- a/src/lib/reasoners/intervals.ml
+++ b/src/lib/reasoners/intervals.ml
@@ -1190,5 +1190,5 @@ module DebugExplanations : Explanations with type t = string list = struct
     List.rev_append l1 l2 |> List.sort_uniq String.compare
 
   let compare l1 l2 =
-    Stdcompat.List.compare String.compare l1 l2
+    Compat.List.compare String.compare l1 l2
 end
diff --git a/src/lib/reasoners/intervals_core.ml b/src/lib/reasoners/intervals_core.ml
index 49c4197ef..a4aaa05e3 100644
--- a/src/lib/reasoners/intervals_core.ml
+++ b/src/lib/reasoners/intervals_core.ml
@@ -190,7 +190,7 @@ module Make(Ex : Explanations) : Core with type explanation = Ex.t = struct
         | NonEmpty i :: u' ->
           if not (Ex.is_empty ex) then Fmt.pf ppf "!%a U@ " Ex.pp ex;
           Interval.pp ppf i;
-          if not (Lists.is_empty u') then Fmt.pf ppf " U@ ";
+          if not (Compat.List.is_empty u') then Fmt.pf ppf " U@ ";
           loop ex u'
       in
       begin match u with
@@ -302,24 +302,24 @@ module Make(Ex : Explanations) : Core with type explanation = Ex.t = struct
         (* i1 is entirely after i2; skip i2
            NB: we never need (i1 U s1) to be a strict subset of s2 because i2 is
            in (i2 U s2) but not in (i1 U s1), making the inclusion strict. *)
-        match Stdcompat.Seq.uncons s2 with
+        match Compat.Seq.uncons s2 with
         | None -> false
         | Some (i2', s2') -> subset_seq ~strict:false i1 s1 i2' s2'
       else
         i2.lb <= i1.lb && i1.ub <= i2.ub &&
         let strict = strict && i1.lb = i2.lb && i1.ub = i2.ub in
-        match Stdcompat.Seq.uncons s1 with
-        | None -> not strict || Option.is_some (Stdcompat.Seq.uncons s2)
+        match Compat.Seq.uncons s1 with
+        | None -> not strict || Option.is_some (Compat.Seq.uncons s2)
         | Some (i1', s1') ->
           if strict then
-            match Stdcompat.Seq.uncons s2 with
+            match Compat.Seq.uncons s2 with
             | None -> false
             | Some (i2', s2') -> subset_seq ~strict:true i1' s1' i2' s2'
           else
             subset_seq ~strict:false i1' s1' i2 s2
 
     let subset ?(strict = false) u1 u2 =
-      let uncons = Stdcompat.Seq.uncons in
+      let uncons = Compat.Seq.uncons in
       match uncons (to_seq u1), uncons (to_seq u2) with
       | None, None -> not strict
       | Some _, None -> false
@@ -328,7 +328,7 @@ module Make(Ex : Explanations) : Core with type explanation = Ex.t = struct
         subset_seq ~strict i1 s1 i2 s2
 
     let equal u1 u2 =
-      Stdcompat.Seq.equal Interval.equal (to_seq u1) (to_seq u2)
+      Compat.Seq.equal Interval.equal (to_seq u1) (to_seq u2)
 
     let checked ((glb, u', gub) as u) =
       let rec loop ex = function
@@ -461,7 +461,7 @@ module Make(Ex : Explanations) : Core with type explanation = Ex.t = struct
         | Empty ex :: u' -> Empty ex :: loop u'
         | NonEmpty i :: u' ->
           let f_i = { lb = f i.lb ; ub = f i.ub } in
-          if Lists.is_empty u' then f_gub := Some f_i.ub;
+          if Compat.List.is_empty u' then f_gub := Some f_i.ub;
           NonEmpty f_i :: loop u'
       in
       let f_u = loop u in
diff --git a/src/lib/reasoners/records.ml b/src/lib/reasoners/records.ml
index 0dc89702e..cb8e11700 100644
--- a/src/lib/reasoners/records.ml
+++ b/src/lib/reasoners/records.ml
@@ -120,7 +120,7 @@ module Shostak (X : ALIEN) = struct
     | Access (a, x, ty) ->
       begin
         match normalize x with
-        | Record (lbs, _) -> Lists.assoc Uid.equal a lbs
+        | Record (lbs, _) -> My_list.assoc Uid.equal a lbs
         | x_n -> Access (a, x_n, ty)
       end
     | Other _ -> v
@@ -252,7 +252,7 @@ module Shostak (X : ALIEN) = struct
   let abstract_access field e ty acc =
     let xe = is_mine e in
     let abs_right_xe, acc =
-      try Lists.assoc X.equal xe acc, acc
+      try My_list.assoc X.equal xe acc, acc
       with Not_found ->
         let left_abs_xe2, acc = X.abstract_selectors xe acc in
         match X.type_info left_abs_xe2 with
@@ -322,7 +322,7 @@ module Shostak (X : ALIEN) = struct
      | Record (lbs, ty) ->
       Record (List.map (fun (n,e') -> n, subst_access x s e') lbs, ty)
      | Access (lb, e', _) when compare_mine x e' = 0 ->
-      Lists.assoc Uid.equal lb s
+      My_list.assoc Uid.equal lb s
      | Access (lb', e', ty) -> Access (lb', subst_access x s e', ty)
      | Other _ -> e
   *)
@@ -359,7 +359,7 @@ module Shostak (X : ALIEN) = struct
 
 
   let orient_solved p v pb =
-    if Lists.mem X.equal p (X.leaves v) then raise Util.Unsolvable;
+    if List.exists (X.equal p) (X.leaves v) then raise Util.Unsolvable;
     Sig.{ pb with sbt = (p,v) :: pb.sbt }
 
   let solve r1 r2 (pb : _ Sig.solve_pb) =
@@ -407,7 +407,7 @@ module Shostak (X : ALIEN) = struct
         (* We can ignore the names of fields as they are inlined in the
            type [ty] of the record. *)
         let l =
-          Lists.try_map (fun (_name, rf) -> to_model_term rf) fields
+          My_list.try_map (fun (_name, rf) -> to_model_term rf) fields
         in
         Option.bind l @@ fun l ->
         Some (E.mk_term Sy.(Op Record) l ty)
diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml
index 8dde0fe60..49e68d6b2 100644
--- a/src/lib/reasoners/satml.ml
+++ b/src/lib/reasoners/satml.ml
@@ -994,7 +994,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 Stdcompat.List.find_opt (fun e ->
+            match List.find_opt (fun e ->
                 let p = get_atom_or_proxy e env.proxies in
                 p.is_true) l
             with
@@ -1865,7 +1865,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
   let is_sat env =
     env.next_dec_guard = Vec.size env.increm_guards &&
     Option.is_none env.next_optimized_split &&
-    Lists.is_empty env.next_decisions &&
+    Compat.List.is_empty env.next_decisions &&
     Option.is_none env.next_split && (
       nb_assigns env = nb_vars env ||
       (Options.get_cdcl_tableaux_inst () &&
diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml
index 8c676fe68..d5e2a5cc1 100644
--- a/src/lib/reasoners/satml_frontend.ml
+++ b/src/lib/reasoners/satml_frontend.ml
@@ -1387,7 +1387,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     | Ty.Tbool ->
       begin
         let bmodel = SAT.boolean_model env.satml in
-        Stdcompat.List.find_map
+        Compat.List.find_map
           (fun Atom.{lit; neg = {lit=neglit; _}; _} ->
              let tlit = Shostak.Literal.make (LTerm t) in
              if Shostak.Literal.equal tlit lit then
diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml
index 39313bf07..e07fc3e1c 100644
--- a/src/lib/structures/expr.ml
+++ b/src/lib/structures/expr.ml
@@ -1348,7 +1348,7 @@ let rec apply_subst_aux (s_t, s_ty) t =
     if Var.Map.is_empty s_t && Ty.M.is_empty s_ty then t
     else
       let s = s_t, s_ty in
-      let xs', same = Lists.apply (apply_subst_aux s) xs in
+      let xs', same = My_list.apply (apply_subst_aux s) xs in
       let ty' = Ty.apply_subst s_ty ty in
       (*invariant: we are sure that the subst will impact xs or ty
          (or inside a lemma/skolem or let) *)
diff --git a/src/lib/structures/modelMap.ml b/src/lib/structures/modelMap.ml
index e84898223..e8fee0f14 100644
--- a/src/lib/structures/modelMap.ml
+++ b/src/lib/structures/modelMap.ml
@@ -93,7 +93,7 @@ module Constraints = struct
     let rec aux ppf seq =
       match seq () with
       | Seq.Nil -> ()
-      | Cons ((ret_val, _), seq) when Stdcompat.Seq.is_empty seq ->
+      | Cons ((ret_val, _), seq) when Compat.Seq.is_empty seq ->
         Fmt.pf ppf "%a" Expr.pp_smtlib ret_val
       | Cons ((ret_val, fiber), seq) ->
         Fmt.pf ppf "(@[<hv>ite %a@ %a@ %a)@]"
diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml
index 5fde2df38..3b00b1e45 100644
--- a/src/lib/structures/symbols.ml
+++ b/src/lib/structures/symbols.ml
@@ -145,7 +145,7 @@ let var s = Var s
 let int i = Int (Z.of_string i)
 let bitv s =
   let biv =
-    Stdcompat.String.fold_left (fun n c ->
+    Compat.String.fold_left (fun n c ->
         match c with
         | '0' -> Z.(n lsl 1)
         | '1' -> Z.((n lsl 1) lor ~$1)
diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml
index 3304f60a4..8daf7a735 100644
--- a/src/lib/structures/ty.ml
+++ b/src/lib/structures/ty.ml
@@ -200,7 +200,7 @@ let rec shorten ty =
   | Tvar { value = Some t'; _ } -> shorten t'
 
   | Text (l,s) ->
-    let l, same = Lists.apply shorten l in
+    let l, same = My_list.apply shorten l in
     if same then ty else Text(l,s)
 
   | Tfarray (t1,t2) ->
@@ -342,7 +342,7 @@ let apply_subst =
       (try M.find n s with Not_found -> ty)
 
     | Text (l,e) ->
-      let l, same = Lists.apply (apply_subst s) l in
+      let l, same = My_list.apply (apply_subst s) l in
       if same then ty else Text(l, e)
 
     | Tfarray (t1,t2) ->
@@ -351,8 +351,8 @@ let apply_subst =
       if t1 == t1' && t2 == t2' then ty else Tfarray (t1', t2')
 
     | Trecord r ->
-      let lbs,  same1 = Lists.apply_right (apply_subst s) r.lbs in
-      let args, same2 = Lists.apply (apply_subst s) r.args in
+      let lbs,  same1 = My_list.apply_right (apply_subst s) r.lbs in
+      let args, same2 = My_list.apply (apply_subst s) r.args in
       if same1 && same2 then ty
       else
         Trecord
diff --git a/src/lib/util/compat.ml b/src/lib/util/compat.ml
new file mode 100644
index 000000000..e428321c4
--- /dev/null
+++ b/src/lib/util/compat.ml
@@ -0,0 +1,127 @@
+(**************************************************************************)
+(*                                                                        *)
+(*                                 OCaml                                  *)
+(*                                                                        *)
+(*             Xavier Leroy, projet Cristal, INRIA Rocquencourt           *)
+(*                                                                        *)
+(*   Copyright 1996 Institut National de Recherche en Informatique et     *)
+(*     en Automatique.                                                    *)
+(*                                                                        *)
+(*   All rights reserved.  This file is distributed under the terms of    *)
+(*   the GNU Lesser General Public License version 2.1, with the          *)
+(*   special exception on linking described in the file LICENSE.          *)
+(*                                                                        *)
+(*     ---------------------------------------------------------------    *)
+(*                                                                        *)
+(*     More details can be found in the directory licenses/               *)
+(*                                                                        *)
+(**************************************************************************)
+
+module List = struct
+  open List
+
+  let is_empty = function
+    | [] -> true
+    | _ -> false
+
+  let rec equal eq l1 l2 =
+    match l1, l2 with
+    | [], [] -> true
+    | [], _::_ | _::_, [] -> false
+    | a1::l1, a2::l2 -> eq a1 a2 && equal eq l1 l2
+
+  let rec compare cmp l1 l2 =
+    match l1, l2 with
+    | [], [] -> 0
+    | [], _::_ -> -1
+    | _::_, [] -> 1
+    | a1::l1, a2::l2 ->
+      let c = cmp a1 a2 in
+      if c <> 0 then c
+      else compare cmp l1 l2
+
+  let rec find_map f = function
+    | [] -> None
+    | x :: l ->
+      begin match f x with
+        | Some _ as result -> result
+        | None -> find_map f l
+      end
+
+  let fold_left_map f accu l =
+    let rec aux accu l_accu = function
+      | [] -> accu, rev l_accu
+      | x :: l ->
+        let accu, x = f accu x in
+        aux accu (x :: l_accu) l in
+    aux accu [] l
+
+  include List [@@@ocaml.warning "-32-33"]
+end
+
+module Bytes = struct
+  open Bytes
+
+  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
+
+  include Bytes [@@@ocaml.warning "-32-33"]
+end
+
+module String = struct
+  open String
+
+  let fold_left f a x =
+    Bytes.fold_left f a (Bytes.unsafe_of_string x)
+
+  let starts_with ~prefix s =
+    let len_s = length s
+    and len_pre = length prefix in
+    let rec aux i =
+      if i = len_pre then true
+      else if not @@ Char.equal (unsafe_get s i) (unsafe_get prefix i) then
+        false
+      else aux (i + 1)
+    in len_s >= len_pre && aux 0
+
+  include String [@@@ocaml.warning "-32-33"]
+end
+
+module Seq = struct
+  open Seq
+
+  let uncons xs =
+    match xs() with
+    | Cons (x, xs) ->
+      Some (x, xs)
+    | Nil ->
+      None
+
+  let is_empty xs =
+    match xs() with
+    | Nil ->
+      true
+    | Cons (_, _) ->
+      false
+
+  let rec append seq1 seq2 () =
+    match seq1() with
+    | Nil -> seq2()
+    | Cons (x, next) -> Cons (x, append next seq2)
+
+  let rec equal eq xs ys =
+    match xs(), ys() with
+    | Nil, Nil ->
+      true
+    | Cons (x, xs), Cons (y, ys) ->
+      eq x y && equal eq xs ys
+    | Nil, Cons (_, _)
+    | Cons (_, _), Nil ->
+      false
+
+  include Seq [@@@ocaml.warning "-32-33"]
+end
diff --git a/src/lib/util/compat.mli b/src/lib/util/compat.mli
new file mode 100644
index 000000000..cc0b1c187
--- /dev/null
+++ b/src/lib/util/compat.mli
@@ -0,0 +1,114 @@
+(**************************************************************************)
+(*                                                                        *)
+(*                                 OCaml                                  *)
+(*                                                                        *)
+(*             Xavier Leroy, projet Cristal, INRIA Rocquencourt           *)
+(*                                                                        *)
+(*   Copyright 1996 Institut National de Recherche en Informatique et     *)
+(*     en Automatique.                                                    *)
+(*                                                                        *)
+(*   All rights reserved.  This file is distributed under the terms of    *)
+(*   the GNU Lesser General Public License version 2.1, with the          *)
+(*   special exception on linking described in the file LICENSE.          *)
+(*                                                                        *)
+(**************************************************************************)
+
+module List : sig
+  val is_empty : 'a list -> bool
+  (** [is_empty l] is true if and only if [l] has no elements. It is equivalent
+      to [compare_length_with l 0 = 0].
+
+      @since OCaml 5.1 *)
+
+  val equal : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool
+  (** [equal eq [a1; ...; an] [b1; ..; bm]] holds when
+      the two input lists have the same length, and for each
+      pair of elements [ai], [bi] at the same position we have
+      [eq ai bi].
+
+      Note: the [eq] function may be called even if the
+      lists have different length. If you know your equality
+      function is costly, you may want to check {!compare_lengths}
+      first.
+
+      @since OCaml 4.12 *)
+
+  val compare : ('a -> 'a -> int) -> 'a list -> 'a list -> int
+  (** [compare cmp [a1; ...; an] [b1; ...; bm]] performs
+      a lexicographic comparison of the two input lists,
+      using the same ['a -> 'a -> int] interface as {!Stdlib.compare}:
+
+      - [a1 :: l1] is smaller than [a2 :: l2] (negative result)
+        if [a1] is smaller than [a2], or if they are equal (0 result)
+        and [l1] is smaller than [l2]
+      - the empty list [[]] is strictly smaller than non-empty lists
+
+      Note: the [cmp] function will be called even if the lists have
+      different lengths.
+
+      @since OCaml 4.12 *)
+
+  val find_map : ('a -> 'b option) -> 'a list -> 'b option
+  (** [find_map f l] applies [f] to the elements of [l] in order,
+      and returns the first result of the form [Some v], or [None]
+      if none exist.
+
+      @since OCaml 4.10 *)
+
+  val fold_left_map :
+    ('acc -> 'a -> 'acc * 'b) -> 'acc -> 'a list -> 'acc * 'b list
+    (** [fold_left_map] is  a combination of [fold_left] and [map] that
+        threads an accumulator through calls to [f].
+
+        @since OCaml 4.11 *)
+end
+
+module String : sig
+  val fold_left : ('acc -> char -> 'acc) -> 'acc -> string -> 'acc
+  (** [fold_left f x s] computes [f (... (f (f x s.[0]) s.[1]) ...) s.[n-1]],
+      where [n] is the length of the string [s].
+
+      @since OCaml 4.13 *)
+
+  val starts_with : prefix :string -> string -> bool
+  (** [starts_with ~prefix s] is [true] if and only if [s] starts with
+      [prefix].
+
+      @since OCaml 4.13 *)
+end
+
+module Seq : sig
+  val uncons : 'a Seq.t -> ('a * 'a Seq.t) option
+  (** If [xs] is empty, then [uncons xs] is [None].
+
+      If [xs] is nonempty, then [uncons xs] is [Some (x, ys)] where [x] is the
+      head of the sequence and [ys] its tail.
+
+      @since OCaml 4.14 *)
+
+  val is_empty : 'a Seq.t -> bool
+  (** [is_empty xs] determines whether the sequence [xs] is empty.
+
+      It is recommended that the sequence [xs] be persistent.
+      Indeed, [is_empty xs] demands the head of the sequence [xs],
+      so, if [xs] is ephemeral, it may be the case that [xs] cannot
+      be used any more after this call has taken place.
+
+      @since OCaml 4.14 *)
+
+  val append : 'a Seq.t -> 'a Seq.t -> 'a Seq.t
+  (** [append xs ys] is the concatenation of the sequences [xs] and [ys].
+
+      Its elements are the elements of [xs], followed by the elements of [ys].
+
+      @since OCaml 4.11 *)
+
+  val equal : ('a -> 'b -> bool) -> 'a Seq.t -> 'b Seq.t -> bool
+  (** Provided the function [eq] defines an equality on elements,
+      [equal eq xs ys] determines whether the sequences [xs] and [ys]
+      are pointwise equal.
+
+      At least one of the sequences [xs] and [ys] must be finite.
+
+      @since OCaml 4.14 *)
+end
diff --git a/src/lib/util/lists.ml b/src/lib/util/my_list.ml
similarity index 95%
rename from src/lib/util/lists.ml
rename to src/lib/util/my_list.ml
index 71418290c..e975150d5 100644
--- a/src/lib/util/lists.ml
+++ b/src/lib/util/my_list.ml
@@ -25,14 +25,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-let is_empty = function
-  | [] -> true
-  | _ -> false
-
-let rec mem eq x = function
-  | [] -> false
-  | a::l -> eq a x || mem eq x l
-
 let rec assoc eq x = function
   | [] -> raise Not_found
   | (a,b)::l -> if eq a x then b else assoc eq x l
diff --git a/src/lib/util/lists.mli b/src/lib/util/my_list.mli
similarity index 94%
rename from src/lib/util/lists.mli
rename to src/lib/util/my_list.mli
index d09854113..12cff3d20 100644
--- a/src/lib/util/lists.mli
+++ b/src/lib/util/my_list.mli
@@ -26,18 +26,11 @@
 (**************************************************************************)
 
 (** Lists utilies
-
     This modules defines some helper functions on lists
 *)
 
 (** {3 Misc functions} *)
 
-val is_empty : 'a list -> bool
-(** Is the list empty? *)
-
-val mem : ('a -> 'a -> bool) -> 'a -> 'a list -> bool
-(** Similar to [List.mem] but use a monomorphic comparison function. *)
-
 val assoc : ('a -> 'a -> bool) -> 'a -> ('a * 'b) list -> 'b
 (** Similar to [List.assoc] but use a monomorphic comparison function. *)
 
diff --git a/src/lib/util/myUnix.ml b/src/lib/util/my_unix.ml
similarity index 100%
rename from src/lib/util/myUnix.ml
rename to src/lib/util/my_unix.ml
diff --git a/src/lib/util/myUnix.mli b/src/lib/util/my_unix.mli
similarity index 99%
rename from src/lib/util/myUnix.mli
rename to src/lib/util/my_unix.mli
index eaa30251d..139463059 100644
--- a/src/lib/util/myUnix.mli
+++ b/src/lib/util/my_unix.mli
@@ -41,4 +41,3 @@ val set_timeout : float -> unit
 
 val unset_timeout : unit -> unit
 (** Unset the previously set timer. *)
-
diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml
index d1131cb2a..ff5400472 100644
--- a/src/lib/util/options.ml
+++ b/src/lib/util/options.ml
@@ -622,16 +622,16 @@ module Time = struct
   let u = ref 0.0
 
   let start () =
-    u := MyUnix.cur_time()
+    u := My_unix.cur_time()
 
   let value () =
-    MyUnix.cur_time () -. !u
+    My_unix.cur_time () -. !u
 
-  let set_timeout tm = MyUnix.set_timeout tm
+  let set_timeout tm = My_unix.set_timeout tm
 
   let unset_timeout () =
     if Float.compare (get_timelimit ()) 0. <> 0 then
-      MyUnix.unset_timeout ()
+      My_unix.unset_timeout ()
 
   let with_timeout tm f =
     Fun.protect
diff --git a/src/lib/util/timers.ml b/src/lib/util/timers.ml
index b7235a3e8..5f5692147 100644
--- a/src/lib/util/timers.ml
+++ b/src/lib/util/timers.ml
@@ -266,7 +266,7 @@ let accumulate_cumulative_mode name env m f cur =
 
 (** save the current timer and start the timer m x f **)
 let start env m f =
-  let cur = MyUnix.cur_time() in
+  let cur = My_unix.cur_time() in
   accumulate_cumulative_mode "start" env m f cur;
   begin
     match env.cur_t with
@@ -280,7 +280,7 @@ let start env m f =
 
 (** pause the timer "m x f" and restore the former timer **)
 let pause env m f =
-  let cur = MyUnix.cur_time() in
+  let cur = My_unix.cur_time() in
   accumulate_cumulative_mode "pause" env m f cur;
   accumulate env cur m f;
   env.cur_u <- cur;
@@ -293,7 +293,7 @@ let pause env m f =
 
 (** update the value of the current timer **)
 let update env =
-  let cur = MyUnix.cur_time() in
+  let cur = My_unix.cur_time() in
   let m, f, _ = env.cur_t in
   accumulate_cumulative_mode "update" env m f cur;
   accumulate env cur m f;