diff --git a/examples/sudoku/sudoku_solve.ml b/examples/sudoku/sudoku_solve.ml
index 761ebc9f..df87a662 100644
--- a/examples/sudoku/sudoku_solve.ml
+++ b/examples/sudoku/sudoku_solve.ml
@@ -1,4 +1,4 @@
-(** {1 simple sudoku solver} *)
+(** simple sudoku solver *)
 
 module Fmt = CCFormat
 module Vec = Sidekick_util.Vec
@@ -179,15 +179,14 @@ end = struct
   end
 
   module Theory = struct
+    include Sidekick_sat.Proof_dummy.Make (F)
+
     type proof = unit
     type proof_step = unit
 
     module Lit = F
 
     type lit = Lit.t
-
-    module Proof = Sidekick_sat.Proof_dummy.Make (Lit)
-
     type t = { grid: Grid.t B_ref.t }
 
     let create g : t = { grid = B_ref.create g }
diff --git a/src/proof-trace/dummy/Sidekick_proof_trace_dummy.ml b/src/proof-trace/dummy/Sidekick_proof_trace_dummy.ml
index da1d2c0c..15b463ed 100644
--- a/src/proof-trace/dummy/Sidekick_proof_trace_dummy.ml
+++ b/src/proof-trace/dummy/Sidekick_proof_trace_dummy.ml
@@ -1,3 +1,7 @@
+(** Dummy proof traces.
+
+    These proof traces will not record information. *)
+
 module type S = Sidekick_sigs_proof_trace.S
 
 module type ARG = sig
@@ -16,3 +20,16 @@ module Make (A : ARG) : S with type t = unit and module A = A = struct
   let add_unsat _ _ = ()
   let delete _ _ = ()
 end
+
+(** Dummy proof trace where everything is [unit]. Use this if you don't care
+   for proofs at all. *)
+module Unit :
+  S with type t = unit and type A.rule = unit and type A.step_id = unit =
+Make (struct
+  type rule = unit
+  type step_id = unit
+
+  module Step_vec = Vec_unit
+
+  let dummy_step_id = ()
+end)
diff --git a/src/sat/Proof_dummy.ml b/src/sat/Proof_dummy.ml
index 7fe4b9f3..947be4b4 100644
--- a/src/sat/Proof_dummy.ml
+++ b/src/sat/Proof_dummy.ml
@@ -1,17 +1,31 @@
-(** Dummy proof module for rule=empty *)
+(** Dummy proof module using rule=[unit].
+
+    These proof traces will not record anything. *)
 
 module Make (Lit : sig
   type t
-end) :
-  Solver_intf.PROOF_RULES
-    with type lit = Lit.t
-     and type rule = unit
-     and type step_id = unit = struct
-  type lit = Lit.t
-  type rule = unit
-  type step_id = unit
+end) : sig
+  module Proof_trace :
+    Sidekick_sigs_proof_trace.S
+      with type A.rule = unit
+       and type A.step_id = unit
+       and type t = unit
 
-  let sat_input_clause _ = ()
-  let sat_redundant_clause _ ~hyps:_ = ()
-  let sat_unsat_core _ = ()
+  module Proof_rules :
+    Solver_intf.PROOF_RULES
+      with type lit = Lit.t
+       and type rule = unit
+       and type step_id = unit
+end = struct
+  module Proof_trace = Sidekick_proof_trace_dummy.Unit
+
+  module Proof_rules = struct
+    type lit = Lit.t
+    type rule = unit
+    type step_id = unit
+
+    let sat_input_clause _ = ()
+    let sat_redundant_clause _ ~hyps:_ = ()
+    let sat_unsat_core _ = ()
+  end
 end
diff --git a/src/sat/dune b/src/sat/dune
index 505da013..b912a7b6 100644
--- a/src/sat/dune
+++ b/src/sat/dune
@@ -1,6 +1,7 @@
 (library
  (name sidekick_sat)
  (public_name sidekick.sat)
- (libraries iter sidekick.util sidekick.core sidekick.sigs.proof-trace)
+ (libraries iter sidekick.util sidekick.core sidekick.sigs.proof-trace
+   sidekick.proof-trace.dummy)
  (synopsis "Pure OCaml SAT solver implementation for sidekick")
  (flags :standard -open Sidekick_util))