From f36aa78a35433dbe4396b90081023872f320bd02 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Thu, 6 Nov 2014 00:20:40 +0100
Subject: [PATCH] In sat/sat, replaced theory state with type unit

---
 sat/sat.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/sat/sat.ml b/sat/sat.ml
index 01105aca..57092e98 100644
--- a/sat/sat.ml
+++ b/sat/sat.ml
@@ -58,16 +58,16 @@ module Tsat = struct
   (* We don't have anything to do since the SAT Solver already
    * does propagation and conflict detection *)
 
-  type t = int
+  type t = unit
   type formula = Fsat.t
   type explanation = Exp.t
   type proof = unit
 
   exception Inconsistent of explanation
 
-  let dummy = -1
-  let empty () = 0
-  let assume ~cs:_ _ _ _ = 0
+  let dummy = ()
+  let empty () = ()
+  let assume ~cs:_ _ _ _ = ()
 end
 
 module Make(Dummy : sig end) = struct