diff --git a/solver/solver.mli b/solver/solver.mli
index 70793d58..05d4b5f0 100644
--- a/solver/solver.mli
+++ b/solver/solver.mli
@@ -14,8 +14,8 @@
 module type S = Solver_intf.S
 
 (** Simple case where the proof type is [unit] and the theory is empty *)
-module DummyTheory(F : Formula_intf.S with type proof = unit) :
-  Theory_intf.S with type formula = F.t and type proof = unit
+module DummyTheory(F : Formula_intf.S) :
+  Theory_intf.S with type formula = F.t and type proof = F.proof
 
 module Make (F : Formula_intf.S)
     (Th : Theory_intf.S with type formula = F.t and type proof = F.proof)