diff --git a/solver/solver.ml b/solver/solver.ml
index b6b53e88..30bb8b1a 100644
--- a/solver/solver.ml
+++ b/solver/solver.ml
@@ -12,12 +12,12 @@
 
 module type S = Solver_intf.S
 
-module DummyTheory(F : Formula_intf.S with type proof = unit) = struct
+module DummyTheory(F : Formula_intf.S) = struct
   (* We don't have anything to do since the SAT Solver already
    * does propagation and conflict detection *)
 
   type formula = F.t
-  type proof = unit
+  type proof = F.proof
   type level = unit
 
   type slice = {