diff --git a/sledge/bin/domain_itv.ml b/sledge/bin/domain_itv.ml
index 91755ae14..8802e12de 100644
--- a/sledge/bin/domain_itv.ml
+++ b/sledge/bin/domain_itv.ml
@@ -45,7 +45,7 @@ let pp fs =
   in
   bindings >> Array.pp "@," (pp_pair Var.print Interval.print) fs
 
-let report_fmt_thunk = Fn.flip pp
+let report_fmt_thunk = Fun.flip pp
 let init _gs = Abstract1.top (Lazy.force man) (Environment.make [||] [||])
 let apron_var_of_name = (fun nm -> "%" ^ nm) >> Apron.Var.of_string
 let apron_var_of_reg = Reg.name >> apron_var_of_name
@@ -134,8 +134,8 @@ and apron_texpr_of_llair_term tm q typ =
         | Div -> Some (mk_arith_binop typ Texpr0.Div)
         | Eq -> Some (mk_bool_binop typ q Tcons0.EQ)
         | Dq -> Some (mk_bool_binop typ q Tcons0.DISEQ)
-        | Lt -> Some (Fn.flip (mk_bool_binop typ q Tcons0.SUP))
-        | Le -> Some (Fn.flip (mk_bool_binop typ q Tcons0.SUPEQ))
+        | Lt -> Some (Fun.flip (mk_bool_binop typ q Tcons0.SUP))
+        | Le -> Some (Fun.flip (mk_bool_binop typ q Tcons0.SUPEQ))
         | _ -> None
       in
       let* te1 = apron_texpr_of_llair_term t1 q typ in
diff --git a/sledge/bin/frontend.ml b/sledge/bin/frontend.ml
index 07078cfaf..da16631a3 100644
--- a/sledge/bin/frontend.ml
+++ b/sledge/bin/frontend.ml
@@ -354,7 +354,7 @@ module Llvalue = struct
   let sexp_of_t llv = Sexp.Atom (Llvm.string_of_llvalue llv)
 end
 
-let struct_rec = Staged.unstage (Exp.struct_rec (module Llvalue))
+let struct_rec = Exp.struct_rec (module Llvalue)
 
 let ptr_fld x ~ptr ~fld ~lltyp =
   let offset =
diff --git a/sledge/bin/sledge.ml b/sledge/bin/sledge.ml
index a5d9e514e..892fdb72f 100644
--- a/sledge/bin/sledge.ml
+++ b/sledge/bin/sledge.ml
@@ -7,7 +7,7 @@
 
 (** SLEdge command line interface *)
 
-let () = Backtrace.Exn.set_recording Version.debug
+let () = Printexc.record_backtrace Version.debug
 
 open Command.Let_syntax
 
diff --git a/sledge/lib/control.ml b/sledge/lib/control.ml
index 7b249acc4..29ff8e0b7 100644
--- a/sledge/lib/control.ml
+++ b/sledge/lib/control.ml
@@ -203,7 +203,7 @@ module Make (Dom : Domain_intf.Dom) = struct
     let pp fs pq =
       Format.fprintf fs "@[%a@]"
         (List.pp " ::@ " pp_priority)
-        (Sequence.to_list (Fheap.to_sequence pq))
+        (Fheap.to_list pq)
 
     let skip _ w = w
     let seq x y d w = y d (x d w)
diff --git a/sledge/lib/domain_intf.ml b/sledge/lib/domain_intf.ml
index 49e8ab76e..0d419052b 100644
--- a/sledge/lib/domain_intf.ml
+++ b/sledge/lib/domain_intf.ml
@@ -10,7 +10,7 @@ module type Dom = sig
   type t [@@deriving equal, sexp_of]
 
   val pp : t pp
-  val report_fmt_thunk : t -> Formatter.t -> unit
+  val report_fmt_thunk : t -> Format.formatter -> unit
   val init : Global.t vector -> t
   val join : t -> t -> t option
   val is_false : t -> bool
diff --git a/sledge/lib/domain_sh.ml b/sledge/lib/domain_sh.ml
index 8ed4ba3ac..fb1187812 100644
--- a/sledge/lib/domain_sh.ml
+++ b/sledge/lib/domain_sh.ml
@@ -10,7 +10,7 @@
 type t = Sh.t [@@deriving equal, sexp]
 
 let pp fs q = Format.fprintf fs "@[{ %a@ }@]" Sh.pp q
-let report_fmt_thunk = Fn.flip pp
+let report_fmt_thunk = Fun.flip pp
 
 (* set by cli *)
 let simplify_states = ref true
diff --git a/sledge/lib/domain_used_globals.ml b/sledge/lib/domain_used_globals.ml
index 4a6d551a6..8f1add5eb 100644
--- a/sledge/lib/domain_used_globals.ml
+++ b/sledge/lib/domain_used_globals.ml
@@ -10,7 +10,7 @@
 type t = Reg.Set.t [@@deriving equal, sexp]
 
 let pp = Reg.Set.pp
-let report_fmt_thunk = Fn.flip pp
+let report_fmt_thunk = Fun.flip pp
 let empty = Reg.Set.empty
 
 let init globals =
diff --git a/sledge/lib/equality.ml b/sledge/lib/equality.ml
index 53066e720..cd1b2fe7b 100644
--- a/sledge/lib/equality.ml
+++ b/sledge/lib/equality.ml
@@ -103,7 +103,7 @@ end = struct
     let exception Found in
     match
       Term.Map.update s e ~f:(function
-        | Some _ -> Exn.raise_without_backtrace Found
+        | Some _ -> raise_notrace Found
         | None -> e )
     with
     | exception Found -> None
@@ -188,10 +188,10 @@ let orient e f =
       let o = compare (height e) (height f) in
       if o <> 0 then o else Term.compare e f
   in
-  match Ordering.of_int (compare e f) with
-  | Less -> Some (e, f)
-  | Equal -> None
-  | Greater -> Some (f, e)
+  match Int.sign (compare e f) with
+  | Neg -> Some (e, f)
+  | Zero -> None
+  | Pos -> Some (f, e)
 
 let norm (_, _, s) e = Subst.norm s e
 
@@ -422,7 +422,7 @@ let congruent r a b =
 let lookup r a =
   [%Trace.call fun {pf} -> pf "%a@ %a" Term.pp a pp r]
   ;
-  ( With_return.with_return
+  ( Base.With_return.with_return
   @@ fun {return} ->
   (* congruent specialized to assume [a] canonized and [b] non-interpreted *)
   let semi_congruent r a b =
@@ -479,7 +479,7 @@ let merge us a b r =
 
 (** find an unproved equation between congruent terms *)
 let find_missing r =
-  With_return.with_return
+  Base.With_return.with_return
   @@ fun {return} ->
   Subst.iteri r.rep ~f:(fun ~key:a ~data:a' ->
       Subst.iteri r.rep ~f:(fun ~key:b ~data:b' ->
diff --git a/sledge/lib/exp.ml b/sledge/lib/exp.ml
index 114be01fd..06c18d60b 100644
--- a/sledge/lib/exp.ml
+++ b/sledge/lib/exp.ml
@@ -480,28 +480,28 @@ let update typ ~rcd idx ~elt =
 
 let struct_rec key =
   let memo_id = Hashtbl.create key in
-  let rec_app = (Staged.unstage (Term.rec_app key)) Term.Record in
-  Staged.stage
-  @@ fun ~id typ elt_thks ->
-  match Hashtbl.find memo_id id with
-  | None ->
-      (* Add placeholder to prevent computing [elts] in calls to
-         [struct_rec] from [elt_thks] for recursive occurrences of [id]. *)
-      let elta = Array.create ~len:(Vector.length elt_thks) null in
-      let elts = Vector.of_array elta in
-      Hashtbl.set memo_id ~key:id ~data:elts ;
-      let term =
-        rec_app ~id (Vector.map ~f:(fun elt -> lazy elt.term) elts)
-      in
-      Vector.iteri elt_thks ~f:(fun i (lazy elt) -> elta.(i) <- elt) ;
-      {desc= ApN (Struct_rec, typ, elts); term} |> check invariant
-  | Some elts ->
-      (* Do not check invariant as invariant will be checked above after the
-         thunks are forced, before which invariant-checking may spuriously
-         fail. Note that it is important that the value constructed here
-         shares the array in the memo table, so that the update after
-         forcing the recursive thunks also updates this value. *)
-      {desc= ApN (Struct_rec, typ, elts); term= rec_app ~id Vector.empty}
+  let rec_app = (Term.rec_app key) Term.Record in
+  fun ~id typ elt_thks ->
+    match Hashtbl.find memo_id id with
+    | None ->
+        (* Add placeholder to prevent computing [elts] in calls to
+           [struct_rec] from [elt_thks] for recursive occurrences of [id]. *)
+        let elta = Array.create ~len:(Vector.length elt_thks) null in
+        let elts = Vector.of_array elta in
+        Hashtbl.set memo_id ~key:id ~data:elts ;
+        let term =
+          rec_app ~id (Vector.map ~f:(fun elt -> lazy elt.term) elts)
+        in
+        Vector.iteri elt_thks ~f:(fun i (lazy elt) -> elta.(i) <- elt) ;
+        {desc= ApN (Struct_rec, typ, elts); term} |> check invariant
+    | Some elts ->
+        (* Do not check invariant as invariant will be checked above after
+           the thunks are forced, before which invariant-checking may
+           spuriously fail. Note that it is important that the value
+           constructed here shares the array in the memo table, so that the
+           update after forcing the recursive thunks also updates this
+           value. *)
+        {desc= ApN (Struct_rec, typ, elts); term= rec_app ~id Vector.empty}
 
 let size_of exp = integer Typ.siz (Z.of_int (Typ.size_of (typ exp)))
 
diff --git a/sledge/lib/exp.mli b/sledge/lib/exp.mli
index d0ef04c48..d7a76cc80 100644
--- a/sledge/lib/exp.mli
+++ b/sledge/lib/exp.mli
@@ -189,7 +189,10 @@ val update : Typ.t -> rcd:t -> int -> elt:t -> t
 
 val struct_rec :
      (module Hashtbl.Key.S with type t = 'id)
-  -> (id:'id -> Typ.t -> t lazy_t vector -> t) Staged.t
+  -> id:'id
+  -> Typ.t
+  -> t lazy_t vector
+  -> t
 (** [struct_rec Id id element_thunks] constructs a possibly-cyclic [Struct]
     value. Cycles are detected using [Id]. The caller of [struct_rec Id]
     must ensure that a single unstaging of [struct_rec Id] is used for each
diff --git a/sledge/lib/import/import.ml b/sledge/lib/import/import.ml
index ddf6d2089..ea365d284 100644
--- a/sledge/lib/import/import.ml
+++ b/sledge/lib/import/import.ml
@@ -7,33 +7,8 @@
 
 (** Global namespace opened in each source file by the build system *)
 
-include (
-  Base :
-    sig
-      include
-        (module type of Base
-          with module Option := Base.Option
-           and module List := Base.List
-           and module Set := Base.Set
-           and module Map := Base.Map
-          (* prematurely deprecated, remove and use Stdlib instead *)
-           and module Filename := Base.Filename
-           and module Format := Base.Format
-           and module Marshal := Base.Marshal
-           and module Scanf := Base.Scanf
-           and type ('ok, 'err) result := ('ok, 'err) Base.result
-         [@warning "-3"])
-    end )
-
-(* undeprecate *)
-external ( == ) : 'a -> 'a -> bool = "%eq"
-external ( != ) : 'a -> 'a -> bool = "%noteq"
-
-exception Not_found = Caml.Not_found
-
 include Stdio
 module Command = Core.Command
-module Hash_queue = Core_kernel.Hash_queue
 include Import0
 
 (** Tuple operations *)
@@ -102,61 +77,41 @@ module Invariant = struct
         with exn ->
           let bt = Caml.Printexc.get_raw_backtrace () in
           let exn =
-            Error.to_exn
-              (Error.create_s
+            Base.Error.to_exn
+              (Base.Error.create_s
                  (Base.Sexp.message "invariant failed"
-                    [ ("", sexp_of_exn exn)
-                    ; ("", Source_code_position.sexp_of_t here)
+                    [ ("", Sexplib.Conv.sexp_of_exn exn)
+                    ; ("", Base.Source_code_position.sexp_of_t here)
                     ; ("", sexp_of_t t) ]))
           in
           Caml.Printexc.raise_with_backtrace exn bt ) ;
       true )
 end
 
-module Option = Option
-include Option.Monad_infix
-include Option.Monad_syntax
-module List = List
-module Vector = Vector
-include Vector.Infix
-module Set = Set
-module Map = Map
-module Qset = Qset
+module Unit = Base.Unit
 
-module Array = struct
-  include Base.Array
+type unit = Unit.t [@@deriving compare, equal, hash, sexp]
 
-  let pp sep pp_elt fs a = List.pp sep pp_elt fs (to_list a)
-end
+module Bool = Base.Bool
 
-module String = struct
-  include String
+type bool = Bool.t [@@deriving compare, equal, hash, sexp]
 
-  let t_of_sexp = Sexplib.Conv.string_of_sexp
-  let sexp_of_t = Sexplib.Conv.sexp_of_string
+module Char = Base.Char
 
-  module Map = Map.Make (String)
-end
+type char = Char.t [@@deriving compare, equal, hash, sexp]
 
-module Q = struct
-  let pp = Q.pp_print
-  let hash = Hashtbl.hash
-  let hash_fold_t s q = Int.hash_fold_t s (hash q)
-  let sexp_of_t q = Sexp.Atom (Q.to_string q)
+module Int = Base.Int
 
-  let t_of_sexp = function
-    | Sexp.Atom s -> Q.of_string s
-    | _ -> assert false
+type int = Int.t [@@deriving compare, equal, hash, sexp]
 
-  let of_z = Q.of_bigint
+module Int64 = Base.Int64
 
-  include Q
-end
+type int64 = Int64.t [@@deriving compare, equal, hash, sexp]
 
 module Z = struct
   let pp = Z.pp_print
   let hash = [%hash: Z.t]
-  let hash_fold_t s z = Int.hash_fold_t s (hash z)
+  let hash_fold_t s z = Hash.fold_int s (hash z)
   let sexp_of_t z = Sexp.Atom (Z.to_string z)
 
   let t_of_sexp = function
@@ -172,3 +127,61 @@ module Z = struct
 
   include Z
 end
+
+module Q = struct
+  let pp = Q.pp_print
+  let hash = Hashtbl.hash
+  let hash_fold_t s q = Hash.fold_int s (hash q)
+  let sexp_of_t q = Sexp.Atom (Q.to_string q)
+
+  let t_of_sexp = function
+    | Sexp.Atom s -> Q.of_string s
+    | _ -> assert false
+
+  let of_z = Q.of_bigint
+
+  include Q
+end
+
+module String = struct
+  module T = struct
+    include Base.String
+
+    let hash_fold_t = Hash.fold_string
+    let hash = Hash.of_fold hash_fold_t
+    let t_of_sexp = Sexplib.Conv.string_of_sexp
+    let sexp_of_t = Sexplib.Conv.sexp_of_string
+  end
+
+  include T
+  module Map = Map.Make (T)
+end
+
+type string = String.t [@@deriving compare, equal, hash, sexp]
+
+module Option = Option
+
+type 'a option = 'a Option.t [@@deriving compare, equal, hash, sexp]
+
+include Option.Monad_infix
+include Option.Monad_syntax
+module Result = Base.Result
+
+module Array = struct
+  include Base.Array
+
+  let pp sep pp_elt fs a = List.pp sep pp_elt fs (to_list a)
+end
+
+module Vector = Vector
+include Vector.Infix
+module List = List
+
+type 'a list = 'a List.t [@@deriving compare, equal, hash, sexp]
+
+module Hash_queue = Core_kernel.Hash_queue
+module Set = Set
+module Hash_set = Base.Hash_set
+module Map = Map
+module Qset = Qset
+module Hashtbl = Base.Hashtbl
diff --git a/sledge/lib/import/import.mli b/sledge/lib/import/import.mli
index 7007170f9..a209923c0 100644
--- a/sledge/lib/import/import.mli
+++ b/sledge/lib/import/import.mli
@@ -7,32 +7,8 @@
 
 (** Global namespace opened in each source file by the build system *)
 
-include module type of (
-  Base :
-    sig
-      include
-        (module type of Base
-          with module Option := Base.Option
-           and module List := Base.List
-           and module Set := Base.Set
-           and module Map := Base.Map
-          (* prematurely deprecated, remove and use Stdlib instead *)
-           and module Filename := Base.Filename
-           and module Format := Base.Format
-           and module Marshal := Base.Marshal
-           and module Scanf := Base.Scanf
-           and type ('ok, 'err) result := ('ok, 'err) Base.result
-         [@warning "-3"])
-    end )
-
-(* undeprecate *)
-
-external ( == ) : 'a -> 'a -> bool = "%eq"
-external ( != ) : 'a -> 'a -> bool = "%noteq"
-
 include module type of Stdio
 module Command = Core.Command
-module Hash_queue = Core_kernel.Hash_queue
 include module type of Import0
 
 (** Tuple operations *)
@@ -106,42 +82,25 @@ val or_error : ('a -> 'b) -> 'a -> unit -> 'b or_error
 (** Extensions *)
 
 module Invariant : module type of Base.Invariant
-module Option = Option
-include module type of Option.Monad_infix
-include module type of Option.Monad_syntax with type 'a t = 'a option
-module List = List
-module Vector = Vector
-include module type of Vector.Infix
-module Set = Set
-module Map = Map
-module Qset = Qset
+module Unit = Base.Unit
 
-module Array : sig
-  include module type of Base.Array
+type unit = Unit.t [@@deriving compare, equal, hash, sexp]
 
-  val pp : (unit, unit) fmt -> 'a pp -> 'a array pp
-end
+module Bool = Base.Bool
 
-module String : sig
-  include module type of String
+type bool = Bool.t [@@deriving compare, equal, hash, sexp]
 
-  val t_of_sexp : Sexp.t -> t
-  val sexp_of_t : t -> Sexp.t
+module Char = Base.Char
 
-  module Map : Map.S with type key = string
-end
+type char = Char.t [@@deriving compare, equal, hash, sexp]
 
-module Q : sig
-  include module type of struct include Q end
+module Int = Base.Int
 
-  val of_z : Z.t -> t
-  val compare : t -> t -> int
-  val hash : t -> int
-  val hash_fold_t : t Hash.folder
-  val t_of_sexp : Sexp.t -> t
-  val sexp_of_t : t -> Sexp.t
-  val pp : t pp
-end
+type int = Int.t [@@deriving compare, equal, hash, sexp]
+
+module Int64 = Base.Int64
+
+type int64 = Int64.t [@@deriving compare, equal, hash, sexp]
 
 module Z : sig
   include module type of struct include Z end
@@ -158,3 +117,52 @@ module Z : sig
   val is_true : t -> bool
   val is_false : t -> bool
 end
+
+module Q : sig
+  include module type of struct include Q end
+
+  val of_z : Z.t -> t
+  val compare : t -> t -> int
+  val hash : t -> int
+  val hash_fold_t : t Hash.folder
+  val t_of_sexp : Sexp.t -> t
+  val sexp_of_t : t -> Sexp.t
+  val pp : t pp
+end
+
+module String : sig
+  include module type of Base.String
+
+  type t = String.t [@@deriving compare, equal, hash, sexp]
+
+  module Map : Map.S with type key = string
+end
+
+type string = String.t [@@deriving compare, equal, hash, sexp]
+
+module Option = Option
+
+type 'a option = 'a Option.t [@@deriving compare, equal, hash, sexp]
+
+include module type of Option.Monad_infix
+include module type of Option.Monad_syntax with type 'a t = 'a option
+module Result = Base.Result
+
+module Array : sig
+  include module type of Base.Array
+
+  val pp : (unit, unit) fmt -> 'a pp -> 'a array pp
+end
+
+module Vector = Vector
+include module type of Vector.Infix
+module List = List
+
+type 'a list = 'a List.t [@@deriving compare, equal, hash, sexp]
+
+module Hash_queue = Core_kernel.Hash_queue
+module Set = Set
+module Hash_set = Base.Hash_set
+module Map = Map
+module Qset = Qset
+module Hashtbl = Base.Hashtbl
diff --git a/sledge/lib/import/import0.ml b/sledge/lib/import/import0.ml
index 8f13d9f27..8f4733599 100644
--- a/sledge/lib/import/import0.ml
+++ b/sledge/lib/import/import0.ml
@@ -5,6 +5,36 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
+module Poly = struct
+  external ( = ) : 'a -> 'a -> bool = "%equal"
+  external ( <> ) : 'a -> 'a -> bool = "%notequal"
+  external ( < ) : 'a -> 'a -> bool = "%lessthan"
+  external ( > ) : 'a -> 'a -> bool = "%greaterthan"
+  external ( <= ) : 'a -> 'a -> bool = "%lessequal"
+  external ( >= ) : 'a -> 'a -> bool = "%greaterequal"
+  external compare : 'a -> 'a -> int = "%compare"
+  external equal : 'a -> 'a -> bool = "%equal"
+
+  let min x y = if x <= y then x else y
+  let max x y = if x >= y then x else y
+end
+
+external ( = ) : int -> int -> bool = "%equal"
+external ( <> ) : int -> int -> bool = "%notequal"
+external ( < ) : int -> int -> bool = "%lessthan"
+external ( > ) : int -> int -> bool = "%greaterthan"
+external ( <= ) : int -> int -> bool = "%lessequal"
+external ( >= ) : int -> int -> bool = "%greaterequal"
+
+let compare (a : int) b =
+  let int_of_bool (b : bool) = (Obj.magic b : int) in
+  int_of_bool (a > b) - int_of_bool (a < b)
+
+external equal : int -> int -> bool = "%equal"
+
+let min x y = if x <= y then x else y
+let max x y = if x >= y then x else y
+
 (** Pretty-printer for argument type. *)
 type 'a pp = Format.formatter -> 'a -> unit
 
diff --git a/sledge/lib/import/list.ml b/sledge/lib/import/list.ml
index e8a925827..258484bac 100644
--- a/sledge/lib/import/list.ml
+++ b/sledge/lib/import/list.ml
@@ -5,15 +5,6 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-open (
-  Base :
-    (module type of Base with module Format := Base.Format [@warning "-3"]) )
-
-(* undeprecate *)
-external ( == ) : 'a -> 'a -> bool = "%eq"
-
-exception Not_found = Caml.Not_found
-
 include Base.List
 
 let rec pp ?pre ?suf sep pp_elt fs = function
@@ -39,7 +30,7 @@ let find_map_remove xs ~f =
   find_map_remove_ [] xs
 
 let fold_option xs ~init ~f =
-  With_return.with_return
+  Base.With_return.with_return
   @@ fun {return} ->
   Some
     (fold xs ~init ~f:(fun acc elt ->
@@ -77,7 +68,7 @@ let rev_map_unzip xs ~f =
       let y, z = f x in
       (y :: ys, z :: zs) )
 
-let remove_exn ?(equal = phys_equal) xs x =
+let remove_exn ?(equal = ( == )) xs x =
   let rec remove_ ys = function
     | [] -> raise Not_found
     | z :: xs ->
@@ -101,17 +92,17 @@ let symmetric_diff ~compare xs ys =
     | x :: xs, y :: ys ->
         let ord = compare x y in
         if ord = 0 then symmetric_diff_ xs ys
-        else if ord < 0 then Either.First x :: symmetric_diff_ xs yys
-        else Either.Second y :: symmetric_diff_ xxs ys
-    | xs, [] -> map ~f:Either.first xs
-    | [], ys -> map ~f:Either.second ys
+        else if ord < 0 then `Left x :: symmetric_diff_ xs yys
+        else `Right y :: symmetric_diff_ xxs ys
+    | xs, [] -> map ~f:(fun x -> `Left x) xs
+    | [], ys -> map ~f:(fun y -> `Right y) ys
   in
   symmetric_diff_ (sort ~compare xs) (sort ~compare ys)
 
 let pp_diff ~compare sep pp_elt fs (xs, ys) =
   let pp_diff_elt fs elt =
-    match (elt : _ Either.t) with
-    | First x -> Format.fprintf fs "-- %a" pp_elt x
-    | Second y -> Format.fprintf fs "++ %a" pp_elt y
+    match elt with
+    | `Left x -> Format.fprintf fs "-- %a" pp_elt x
+    | `Right y -> Format.fprintf fs "++ %a" pp_elt y
   in
   pp sep pp_diff_elt fs (symmetric_diff ~compare xs ys)
diff --git a/sledge/lib/import/list.mli b/sledge/lib/import/list.mli
index 3643920d3..af00b0831 100644
--- a/sledge/lib/import/list.mli
+++ b/sledge/lib/import/list.mli
@@ -5,7 +5,6 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-open Base
 include module type of Base.List
 open Import0
 
@@ -54,4 +53,7 @@ val remove : ?equal:('a -> 'a -> bool) -> 'a list -> 'a -> 'a list option
 val rev_init : int -> f:(int -> 'a) -> 'a list
 
 val symmetric_diff :
-  compare:('a -> 'a -> int) -> 'a t -> 'a t -> ('a, 'a) Either.t t
+     compare:('a -> 'a -> int)
+  -> 'a t
+  -> 'a t
+  -> [`Left of 'a | `Right of 'a] t
diff --git a/sledge/lib/import/option.ml b/sledge/lib/import/option.ml
index ffa0bd68f..8c441ce56 100644
--- a/sledge/lib/import/option.ml
+++ b/sledge/lib/import/option.ml
@@ -5,10 +5,6 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-open (
-  Base :
-    (module type of Base with module Format := Base.Format [@warning "-3"]) )
-
 include Base.Option
 
 let pp fmt pp_elt fs = function
diff --git a/sledge/lib/import/option.mli b/sledge/lib/import/option.mli
index ac2eb9d2c..94886e0c8 100644
--- a/sledge/lib/import/option.mli
+++ b/sledge/lib/import/option.mli
@@ -5,7 +5,6 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-open Base
 open Import0
 include module type of Base.Option
 
diff --git a/sledge/lib/import/vector.ml b/sledge/lib/import/vector.ml
index 272be639d..531be5c4f 100644
--- a/sledge/lib/import/vector.ml
+++ b/sledge/lib/import/vector.ml
@@ -7,7 +7,10 @@
 
 (** Vector - Immutable view of an array *)
 
-open (Base : module type of Base with module List := Base.List)
+module Array = Base.Array
+module Hash = Base.Hash
+module With_return = Base.With_return
+open Base.Continue_or_stop
 
 (** = 'a array but covariant since imperative operations hidden *)
 type +'a t
@@ -47,8 +50,8 @@ let map_adjacent ~f dummy xs_v =
             xs
       in
       map_adjacent_ (i + 1) xs
-    else if phys_equal xs xs0 then xs
-    else Array.filter xs ~f:(fun x -> not (phys_equal dummy x))
+    else if xs == xs0 then xs
+    else Array.filter xs ~f:(fun x -> not (dummy == x))
   in
   v (map_adjacent_ 0 xs0)
 
@@ -91,7 +94,7 @@ let map_preserving_phys_equal xs ~f =
   let xs' =
     map xs ~f:(fun x ->
         let x' = f x in
-        if not (phys_equal x' x) then change := true ;
+        if not (x' == x) then change := true ;
         x' )
   in
   if !change then xs' else xs
@@ -108,9 +111,7 @@ let fold_map_until xs ~init ~f ~finish =
   With_return.with_return (fun {return} ->
       finish
         (fold_map xs ~init ~f:(fun s x ->
-             match (f s x : _ Continue_or_stop.t) with
-             | Continue x -> x
-             | Stop x -> return x )) )
+             match f s x with Continue x -> x | Stop x -> return x )) )
 
 let concat xs = v (Array.concat (al xs))
 let copy x = v (Array.copy (a x))
diff --git a/sledge/lib/import/vector.mli b/sledge/lib/import/vector.mli
index 79bc51a94..66939b8f4 100644
--- a/sledge/lib/import/vector.mli
+++ b/sledge/lib/import/vector.mli
@@ -11,7 +11,6 @@
     Vector is not a safe immutable data structure, it only attempts to make
     it inconvenient to mutate. *)
 
-open Base
 open Import0
 
 type +'a t [@@deriving compare, equal, hash, sexp]
@@ -45,7 +44,7 @@ val fold_result :
 val fold_until :
      'a t
   -> init:'accum
-  -> f:('accum -> 'a -> ('accum, 'final) Continue_or_stop.t)
+  -> f:('accum -> 'a -> ('accum, 'final) Base.Continue_or_stop.t)
   -> finish:('accum -> 'final)
   -> 'final
 
@@ -115,7 +114,7 @@ val map_preserving_phys_equal : 'a t -> f:('a -> 'a) -> 'a t
 val fold_map_until :
      'a t
   -> init:'accum
-  -> f:('accum -> 'a -> ('accum * 'b, 'final) Continue_or_stop.t)
+  -> f:('accum -> 'a -> ('accum * 'b, 'final) Base.Continue_or_stop.t)
   -> finish:('accum * 'b t -> 'final)
   -> 'final
 
diff --git a/sledge/lib/report.ml b/sledge/lib/report.ml
index df0ea6a01..2f42f8c53 100644
--- a/sledge/lib/report.ml
+++ b/sledge/lib/report.ml
@@ -26,7 +26,7 @@ let count = ref 0
 let invalid_access_count () = !count
 
 let invalid_access fmt_thunk pp access loc =
-  Int.incr count ;
+  incr count ;
   let rep fs =
     Format.fprintf fs "%a Invalid memory access@;<1 2>@[%a@]" Loc.pp
       (loc access) pp access
diff --git a/sledge/lib/report.mli b/sledge/lib/report.mli
index 941b268c6..9c37995bc 100644
--- a/sledge/lib/report.mli
+++ b/sledge/lib/report.mli
@@ -8,6 +8,6 @@
 (** Issue reporting *)
 
 val unknown_call : Llair.term -> unit
-val invalid_access_inst : (Formatter.t -> unit) -> Llair.inst -> unit
-val invalid_access_term : (Formatter.t -> unit) -> Llair.term -> unit
+val invalid_access_inst : (Format.formatter -> unit) -> Llair.inst -> unit
+val invalid_access_term : (Format.formatter -> unit) -> Llair.term -> unit
 val invalid_access_count : unit -> int
diff --git a/sledge/lib/sh.ml b/sledge/lib/sh.ml
index d36ca44d6..0e53ac0e9 100644
--- a/sledge/lib/sh.ml
+++ b/sledge/lib/sh.ml
@@ -644,7 +644,7 @@ let rec norm_ s q =
   [%Trace.call fun {pf} -> pf "@[%a@]@ %a" Equality.Subst.pp s pp_raw q]
   ;
   let q =
-    map q ~f_sjn:(norm_ s) ~f_cong:Fn.id ~f_trm:(Equality.Subst.subst s)
+    map q ~f_sjn:(norm_ s) ~f_cong:Fun.id ~f_trm:(Equality.Subst.subst s)
   in
   let xs, cong = Equality.apply_subst (Var.Set.union q.us q.xs) s q.cong in
   exists_fresh xs {q with cong}
diff --git a/sledge/lib/term.ml b/sledge/lib/term.ml
index f41e3b268..7375a4587 100644
--- a/sledge/lib/term.ml
+++ b/sledge/lib/term.ml
@@ -231,8 +231,8 @@ let assert_monomial mono =
   | Mul args ->
       Qset.iter args ~f:(fun factor exponent ->
           assert (Q.sign exponent > 0) ;
-          assert_indeterminate factor |> Fn.id )
-  | _ -> assert_indeterminate mono |> Fn.id
+          assert_indeterminate factor |> Fun.id )
+  | _ -> assert_indeterminate mono |> Fun.id
 
 (* a polynomial term is a monomial multiplied by a non-zero coefficient
  *     c × ∏ᵢ xᵢ
@@ -246,8 +246,8 @@ let assert_poly_term mono coeff =
       | None | Some (Integer _, _) -> assert false
       | Some (_, n) -> assert (Qset.length args > 1 || not (Q.equal Q.one n))
       ) ;
-      assert_monomial mono |> Fn.id
-  | _ -> assert_monomial mono |> Fn.id
+      assert_monomial mono |> Fun.id
+  | _ -> assert_monomial mono |> Fun.id
 
 (* a polynomial is a linear combination of monomials, e.g.
  *     ∑ᵢ cᵢ × ∏ⱼ xᵢⱼ
@@ -261,7 +261,7 @@ let assert_polynomial poly =
       | None | Some (Integer _, _) -> assert false
       | Some (_, k) -> assert (Qset.length args > 1 || not (Q.equal Q.one k))
       ) ;
-      Qset.iter args ~f:(fun m c -> assert_poly_term m c |> Fn.id)
+      Qset.iter args ~f:(fun m c -> assert_poly_term m c |> Fun.id)
   | _ -> assert false
 
 (* aggregate args of Extract and Concat must be aggregate terms, in
@@ -278,8 +278,8 @@ let invariant e =
   Invariant.invariant [%here] e [%sexp_of: t]
   @@ fun () ->
   match e with
-  | Add _ -> assert_polynomial e |> Fn.id
-  | Mul _ -> assert_monomial e |> Fn.id
+  | Add _ -> assert_polynomial e |> Fun.id
+  | Mul _ -> assert_monomial e |> Fun.id
   | Ap2 (Memory, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _) ->
       assert_aggregate e
   | ApN (Record, elts) | RecN (Record, elts) ->
@@ -788,10 +788,10 @@ let simp_uno x y = Ap2 (Uno, x, y)
 
 let rec simp_eq x y =
   match
-    match Ordering.of_int (compare x y) with
-    | Equal -> None
-    | Less -> Some (x, y)
-    | Greater -> Some (y, x)
+    match Int.sign (compare x y) with
+    | Zero -> None
+    | Neg -> Some (x, y)
+    | Pos -> Some (y, x)
   with
   (* e = e ==> true *)
   | None -> bool true
@@ -934,24 +934,24 @@ let simp_update idx rcd elt = Ap2 (Update idx, rcd, elt)
 let rec_app key =
   let memo_id = Hashtbl.create key in
   let dummy = null in
-  Staged.stage
-  @@ fun ~id op elt_thks ->
-  match Hashtbl.find memo_id id with
-  | None ->
-      (* Add placeholder to prevent computing [elts] in calls to [rec_app]
-         from [elt_thks] for recursive occurrences of [id]. *)
-      let elta = Array.create ~len:(Vector.length elt_thks) dummy in
-      let elts = Vector.of_array elta in
-      Hashtbl.set memo_id ~key:id ~data:elts ;
-      Vector.iteri elt_thks ~f:(fun i (lazy elt) -> elta.(i) <- elt) ;
-      RecN (op, elts) |> check invariant
-  | Some elts ->
-      (* Do not check invariant as invariant will be checked above after the
-         thunks are forced, before which invariant-checking may spuriously
-         fail. Note that it is important that the value constructed here
-         shares the array in the memo table, so that the update after
-         forcing the recursive thunks also updates this value. *)
-      RecN (op, elts)
+  fun ~id op elt_thks ->
+    match Hashtbl.find memo_id id with
+    | None ->
+        (* Add placeholder to prevent computing [elts] in calls to [rec_app]
+           from [elt_thks] for recursive occurrences of [id]. *)
+        let elta = Array.create ~len:(Vector.length elt_thks) dummy in
+        let elts = Vector.of_array elta in
+        Hashtbl.set memo_id ~key:id ~data:elts ;
+        Vector.iteri elt_thks ~f:(fun i (lazy elt) -> elta.(i) <- elt) ;
+        RecN (op, elts) |> check invariant
+    | Some elts ->
+        (* Do not check invariant as invariant will be checked above after
+           the thunks are forced, before which invariant-checking may
+           spuriously fail. Note that it is important that the value
+           constructed here shares the array in the memo table, so that the
+           update after forcing the recursive thunks also updates this
+           value. *)
+        RecN (op, elts)
 
 (* dispatching for normalization and invariant checking *)
 
diff --git a/sledge/lib/term.mli b/sledge/lib/term.mli
index a14b13e10..71bb6a822 100644
--- a/sledge/lib/term.mli
+++ b/sledge/lib/term.mli
@@ -221,7 +221,10 @@ val update : rcd:t -> idx:int -> elt:t -> t
 (* recursive n-ary application *)
 val rec_app :
      (module Hashtbl.Key.S with type t = 'id)
-  -> (id:'id -> recN -> t lazy_t vector -> t) Staged.t
+  -> id:'id
+  -> recN
+  -> t lazy_t vector
+  -> t
 
 val size_of : Typ.t -> t
 
diff --git a/sledge/ppx_trace/ppx_trace.ml b/sledge/ppx_trace/ppx_trace.ml
index 274b6058c..2a382b82d 100644
--- a/sledge/ppx_trace/ppx_trace.ml
+++ b/sledge/ppx_trace/ppx_trace.ml
@@ -83,7 +83,7 @@ let mapper =
   in
   let expr (m : Ast_mapper.mapper) exp =
     let append_here_args args =
-      let mod_name = evar ~loc:Location.none "Caml.__MODULE__" in
+      let mod_name = evar ~loc:Location.none "Stdlib.__MODULE__" in
       let fun_name =
         estring ~loc:Location.none (get_fun_name (vb_stack_top ()))
       in
@@ -117,7 +117,7 @@ let mapper =
     | Pexp_extension
         ( {txt= "Trace.retn"; loc= retn_loc}
         , PStr [{pstr_desc= Pstr_eval (retn_fun, []); _}] ) ->
-        if not !debug then evar ~loc:exp.pexp_loc "Fn.id"
+        if not !debug then evar ~loc:exp.pexp_loc "Stdlib.Fun.id"
         else
           pexp_apply ~loc:exp.pexp_loc
             (evar ~loc:retn_loc "Trace.retn")