diff --git a/src/base/th_data.ml b/src/base/th_data.ml
index 1001ce21..87dede54 100644
--- a/src/base/th_data.ml
+++ b/src/base/th_data.ml
@@ -4,7 +4,6 @@ open Sidekick_core
 
 let arg =
   (module struct
-    module S = Solver
     open! Sidekick_th_data
     open Data_ty
     module Cstor = Cstor
diff --git a/src/base/th_lra.ml b/src/base/th_lra.ml
index 933b482e..25c5e587 100644
--- a/src/base/th_lra.ml
+++ b/src/base/th_lra.ml
@@ -3,7 +3,6 @@
 open Sidekick_core
 module T = Term
 module Q = Sidekick_zarith.Rational
-open LRA_term
 
 let mk_eq = Form.eq
 let mk_bool = T.bool
diff --git a/src/core/proof_trace.mli b/src/core/proof_trace.mli
index 67ef05cb..b276f1e4 100644
--- a/src/core/proof_trace.mli
+++ b/src/core/proof_trace.mli
@@ -6,8 +6,6 @@
     to its premises.
 *)
 
-open Sidekick_core_logic
-
 type lit = Lit.t
 
 type step_id = Proof_step.id
diff --git a/src/sat/store.mli b/src/sat/store.mli
index 73be49e3..112f075f 100644
--- a/src/sat/store.mli
+++ b/src/sat/store.mli
@@ -1,5 +1,4 @@
 open Sidekick_core
-open Sigs
 
 type var = Base_types_.var
 type atom = Base_types_.atom
diff --git a/src/smt/model_builder.mli b/src/smt/model_builder.mli
index f149a916..592a73c9 100644
--- a/src/smt/model_builder.mli
+++ b/src/smt/model_builder.mli
@@ -6,7 +6,6 @@
   TODO: seen values?
 *)
 
-open Sidekick_core
 open Sigs
 
 type t