From 1ce3973f9eaa4a47fd7efcd5084302576af40493 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Fri, 15 Apr 2016 14:02:18 +0200
Subject: [PATCH] [feature] Allow arbitrary proof types in DummyTheory

---
 solver/solver.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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 = {