missing change

Author: c-cube

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)