diff --git a/src/th-lra/sidekick_th_lra.ml b/src/th-lra/sidekick_th_lra.ml
index d1666f2d..5d60f300 100644
--- a/src/th-lra/sidekick_th_lra.ml
+++ b/src/th-lra/sidekick_th_lra.ml
@@ -4,11 +4,9 @@
 open Sidekick_core
 open Sidekick_cc
 module Intf = Intf
-open Intf
+include Intf
 module SI = SMT.Solver_internal
 
-module type ARG = Intf.ARG
-
 module Tag = struct
   type t = Lit of Lit.t | CC_eq of E_node.t * E_node.t
 
diff --git a/src/th-lra/sidekick_th_lra.mli b/src/th-lra/sidekick_th_lra.mli
index fdb34b33..11ee0b4c 100644
--- a/src/th-lra/sidekick_th_lra.mli
+++ b/src/th-lra/sidekick_th_lra.mli
@@ -1,9 +1,10 @@
 (** Linear Rational Arithmetic *)
 
 module Intf = Intf
-open Intf
 
-module type ARG = Intf.ARG
+include module type of struct
+  include Intf
+end
 
 (* TODO
    type state