diff --git a/sat/explanation.ml b/sat/explanation.ml
index c3a552c1..aec8b4f7 100644
--- a/sat/explanation.ml
+++ b/sat/explanation.ml
@@ -28,7 +28,7 @@ module Make(Stypes : Solver_types.S) = struct
         | Atom _, Fresh _ -> -1
         | Fresh _, Atom _ -> 1
         | Fresh i1, Fresh i2 -> i1 - i2
-        | Atom a, Atom b -> a.aid - b.aid
+        | Atom a, Atom b -> Stypes.(a.aid - b.aid)
     end)
 
   type t = S.t
diff --git a/sat/formula_intf.ml b/sat/formula_intf.ml
index 03834ae8..e6b78260 100644
--- a/sat/formula_intf.ml
+++ b/sat/formula_intf.ml
@@ -34,8 +34,5 @@ module type S = sig
   val add_label : Hstring.t -> t -> unit
 
   val print : Format.formatter -> t -> unit
-
-  module Map : Map.S with type key = t
-
 end
 
diff --git a/sat/solver.ml b/sat/solver.ml
index aa184bab..357e29b2 100644
--- a/sat/solver.ml
+++ b/sat/solver.ml
@@ -951,3 +951,4 @@ module Make (F : Formula_intf.S)
     if negated then not truth else truth
 
 end
+
diff --git a/sat/solver_types.ml b/sat/solver_types.ml
index de5a1688..84b09c77 100644
--- a/sat/solver_types.ml
+++ b/sat/solver_types.ml
@@ -83,7 +83,7 @@ module Make (F : Formula_intf.S) = struct
       learnt = false;
       cpremise = [] }
 
-  module MA = F.Map
+  module MA = Map.Make(F)
   type varmap = var MA.t
 
   let ale = Hstring.make "<="
@@ -158,19 +158,6 @@ module Make (F : Formula_intf.S) = struct
     let cpt = ref 0 in
     fun () -> incr cpt; "C" ^ (string_of_int !cpt)
 
-
-
-  module Clause = struct
-
-    let size c = Vec.size c.atoms
-    let pop c = Vec.pop c.atoms
-    let shrink c i = Vec.shrink  c.atoms i
-    let last c = Vec.last c.atoms
-    let get c i = Vec.get c.atoms i
-    let set c i v = Vec.set c.atoms i v
-
-  end
-
   let to_float i = float_of_int i
 
   let to_int f = int_of_float f