diff --git a/TODO.md b/TODO.md
index 0d0f0916..ec05fdb5 100644
--- a/TODO.md
+++ b/TODO.md
@@ -14,3 +14,4 @@
 
 - max-sat/max-smt
 - coq proofs ?
+
diff --git a/backend/backend_intf.ml b/backend/backend_intf.ml
index 82205f94..81957d78 100644
--- a/backend/backend_intf.ml
+++ b/backend/backend_intf.ml
@@ -1,15 +1,6 @@
 
-module type Arg = sig
-  type proof
-  type formula
-  val prove : Format.formatter -> formula list -> unit
-  val context : Format.formatter -> proof -> unit
-  val translate : Format.formatter -> formula -> unit
-end
-
 module type S = sig
   type t
   val print : Format.formatter -> t -> unit
 end
 
-
diff --git a/backend/dedukti.ml b/backend/dedukti.ml
index 107d9fe5..6b219c15 100644
--- a/backend/dedukti.ml
+++ b/backend/dedukti.ml
@@ -6,7 +6,15 @@ Copyright 2014 Simon Cruanes
 
 module type S = Backend_intf.S
 
-module Make(S : Res.S)(A : Backend_intf.Arg with type formula := S.atom and type proof := S.proof) = struct
+module type Arg = sig
+  type proof
+  type formula
+  val prove : Format.formatter -> formula list -> unit
+  val context : Format.formatter -> proof -> unit
+  val translate : Format.formatter -> formula -> unit
+end
+
+module Make(S : Res.S)(A : Arg with type formula := S.atom and type proof := S.proof) = struct
 
   let print_aux fmt = Format.fprintf fmt "@\n"
 
diff --git a/backend/dedukti.mli b/backend/dedukti.mli
index 9f1b3ee9..3a14b23e 100644
--- a/backend/dedukti.mli
+++ b/backend/dedukti.mli
@@ -1,8 +1,16 @@
 
 module type S = Backend_intf.S
 
+module type Arg = sig
+  type proof
+  type formula
+  val prove : Format.formatter -> formula list -> unit
+  val context : Format.formatter -> proof -> unit
+  val translate : Format.formatter -> formula -> unit
+end
+
 module Make :
   functor(S : Res.S) ->
-  functor(A : Backend_intf.Arg with type formula := S.atom and type proof := S.proof) ->
+  functor(A : Arg with type formula := S.atom and type proof := S.proof) ->
     S with type t := S.proof
 (** Functor to generate a backend to output proofs for the dedukti type checker. *)
diff --git a/backend/dot.ml b/backend/dot.ml
index 8a00ef27..ab8ca4a7 100644
--- a/backend/dot.ml
+++ b/backend/dot.ml
@@ -1,15 +1,19 @@
 
 module type S = Backend_intf.S
 
-module Make
-    (St : Solver_types.S)
-    (S : Res.S with type clause = St.clause
-                and type lemma = St.proof
-                and type atom = St.atom) = struct
+module type Arg = sig
+  type atom
+  type clause
+  type lemma
 
-  let clause_id c = St.(c.name)
+  val clause_name : clause -> string
+  val print_atom : Format.formatter -> atom -> unit
+  val lemma_info : lemma -> string * string option * atom list
+end
 
-  let node_id n = clause_id S.(n.conclusion)
+module Make(S : Res.S)(A : Arg with type atom := S.atom and type clause := S.clause and type lemma := S.lemma) = struct
+
+  let node_id n = A.clause_name S.(n.conclusion)
 
   let res_node_id n = (node_id n) ^ "_res"
 
@@ -43,7 +47,7 @@ module Make
       id table_options color table (c, rule, rule_color, l)
 
   let print_dot_res_node fmt id a =
-    Format.fprintf fmt "%s [label=\"%a\"];@\n" id St.print_atom a
+    Format.fprintf fmt "%s [label=\"%a\"];@\n" id A.print_atom a
 
   let ttify f c = fun fmt () -> f fmt c
 
@@ -51,16 +55,15 @@ module Make
     match S.(n.step) with
     | S.Hypothesis ->
       print_dot_node fmt (node_id n) "LIGHTBLUE" S.(n.conclusion) "Hypothesis" "LIGHTBLUE"
-        [(fun fmt () -> (Format.fprintf fmt "%s" n.S.conclusion.St.name))];
+        [(fun fmt () -> (Format.fprintf fmt "%s" (A.clause_name n.S.conclusion)))];
     | S.Lemma lemma ->
-      let rule, f_args, t_args, color = St.proof_debug lemma in
+      let rule, color, args = A.lemma_info lemma in
       let color = match color with None -> "YELLOW" | Some c -> c in
-      let l = List.map (ttify St.print_atom) f_args @
-              List.map (ttify St.print_lit) t_args in
+      let l = List.map (ttify A.print_atom) args in
       print_dot_node fmt (node_id n) "LIGHTBLUE" S.(n.conclusion) rule color l
     | S.Resolution (_, _, a) ->
       print_dot_node fmt (node_id n) "GREY" S.(n.conclusion) "Resolution" "GREY"
-        [(fun fmt () -> (Format.fprintf fmt "%s" n.S.conclusion.St.name))];
+        [(fun fmt () -> (Format.fprintf fmt "%s" (A.clause_name n.S.conclusion)))];
       print_dot_res_node fmt (res_node_id n) a;
       print_edge fmt (node_id n) (res_node_id n)
 
diff --git a/backend/dot.mli b/backend/dot.mli
new file mode 100644
index 00000000..10ee95ef
--- /dev/null
+++ b/backend/dot.mli
@@ -0,0 +1,16 @@
+
+module type S = Backend_intf.S
+
+module type Arg = sig
+  type atom
+  type clause
+  type lemma
+
+  val clause_name : clause -> string
+  val print_atom : Format.formatter -> atom -> unit
+  val lemma_info : lemma -> string * string option * atom list
+end
+
+module Make(S : Res.S)(A : Arg with type atom := S.atom and type clause := S.clause and type lemma := S.lemma) :
+  S with type t := S.proof
+
diff --git a/msat.odocl b/msat.odocl
index 677dea71..6cf3a141 100644
--- a/msat.odocl
+++ b/msat.odocl
@@ -2,25 +2,24 @@ util/Log
 
 solver/Log_intf
 solver/Formula_intf
-solver/Expr_intf
-
-solver/Res
-solver/Res_intf
-solver/Mcproof
-
-solver/Solver
-solver/Solver_types
-solver/Solver_types_intf
-solver/Mcsolver
-solver/Mcsolver_types
-solver/Mcsolver_types_intf
-
 solver/Theory_intf
 solver/Plugin_intf
-
-solver/Tseitin
+solver/Expr_intf
 solver/Tseitin_intf
+solver/Res_intf
+solver/Solver_types_intf
+
+solver/Internal
+solver/Solver
+solver/Mcsolver
+solver/Solver_types
+
+solver/Res
+solver/Tseitin
+
+backend/Dot
+backend/Dedukti
+backend/Backend_intf
 
 sat/Sat
 
-backend/Dedukti
diff --git a/sat/sat.ml b/sat/sat.ml
index 40731ee6..6348ffe4 100644
--- a/sat/sat.ml
+++ b/sat/sat.ml
@@ -8,6 +8,7 @@ module Fsat = struct
   exception Dummy of int
 
   type t = int
+  type proof = unit
 
   let max_lit = max_int
   let max_fresh = ref (-1)
@@ -90,7 +91,11 @@ end
 module Make(Log : Log_intf.S) = struct
 
   module SatSolver = Solver.Make(Log)(Fsat)(Tsat)
-  module Dot = Dot.Make(SatSolver.St)(SatSolver.Proof)
+  module Dot = Dot.Make(SatSolver.Proof)(struct
+      let clause_name c = SatSolver.St.(c.name)
+      let print_atom = SatSolver.St.print_atom
+      let lemma_info () = "()", None, []
+    end)
 
   exception Bad_atom
 
diff --git a/smt/expr.ml b/smt/expr.ml
index b61c62bd..9e13da2d 100644
--- a/smt/expr.ml
+++ b/smt/expr.ml
@@ -12,6 +12,7 @@ type formula =
     | Equal of var * var
     | Distinct of var * var
 type t = formula
+type proof = unit
 
 let dummy = Prop 0
 
diff --git a/smt/expr.mli b/smt/expr.mli
index cff2bf41..a62cf5ea 100644
--- a/smt/expr.mli
+++ b/smt/expr.mli
@@ -11,6 +11,7 @@ type formula = private
     | Distinct of var * var
 
 type t = formula
+type proof = unit
 
 val dummy : t
 
diff --git a/smt/mcsat.ml b/smt/mcsat.ml
index ce4fd320..257682ea 100644
--- a/smt/mcsat.ml
+++ b/smt/mcsat.ml
@@ -14,12 +14,8 @@ module Tsmt = struct
   (* Type definitions *)
   type term = Fsmt.Term.t
   type formula = Fsmt.t
-
   type proof = unit
 
-  let proof_debug () =
-      "Proof", [], ["..."], Some "PURPLE"
-
   type assumption =
     | Lit of formula
     | Assign of term * term
@@ -115,7 +111,11 @@ end
 module Make(Dummy:sig end) = struct
 
   module SmtSolver = Mcsolver.Make(Log)(Fsmt)(Tsmt)
-  module Dot = Dot.Make(SmtSolver.St)(SmtSolver.Proof)
+  module Dot = Dot.Make(SmtSolver.Proof)(struct
+      let clause_name c = SmtSolver.St.(c.name)
+      let print_atom = SmtSolver.St.print_atom
+      let lemma_info () = "Proof", Some "PURPLE", []
+    end)
 
   type atom = Fsmt.t
   type clause = SmtSolver.St.clause
diff --git a/smt/smt.ml b/smt/smt.ml
index 6ef3ad7f..85733eee 100644
--- a/smt/smt.ml
+++ b/smt/smt.ml
@@ -61,7 +61,11 @@ end
 module Make(Dummy:sig end) = struct
 
   module SmtSolver = Solver.Make(Log)(Fsmt)(Tsmt)
-  module Dot = Dot.Make(SmtSolver.St)(SmtSolver.Proof)
+  module Dot = Dot.Make(SmtSolver.Proof)(struct
+      let clause_name c = SmtSolver.St.(c.name)
+      let print_atom = SmtSolver.St.print_atom
+      let lemma_info () = "Proof", Some "PURPLE", []
+    end)
 
   type atom = Fsmt.t
   type clause = SmtSolver.St.clause
diff --git a/solver/expr_intf.ml b/solver/expr_intf.ml
index 1117b05b..d5852ede 100644
--- a/solver/expr_intf.ml
+++ b/solver/expr_intf.ml
@@ -25,6 +25,9 @@ module type S = sig
     val print : Format.formatter -> t -> unit
   end
 
+  type proof
+  (** An abstract type for proofs *)
+
   val dummy : Formula.t
   (** Formula constants. A valid formula should never be physically equal to [dummy] *)
 
diff --git a/solver/formula_intf.ml b/solver/formula_intf.ml
index 044f1ac2..d8da5664 100644
--- a/solver/formula_intf.ml
+++ b/solver/formula_intf.ml
@@ -10,6 +10,9 @@ module type S = sig
   type t
   (** The type of atomic formulas. *)
 
+  type proof
+  (** An abstract type for proofs *)
+
   val dummy : t
   (** Formula constants. A valid formula should never be physically equal to [dummy] *)
 
diff --git a/solver/internal.ml b/solver/internal.ml
index 6ce611b9..ccdb3f32 100644
--- a/solver/internal.ml
+++ b/solver/internal.ml
@@ -7,9 +7,10 @@ Copyright 2014 Simon Cruanes
 module Make (L : Log_intf.S)(St : Solver_types.S)
     (Th : Plugin_intf.S with type term = St.term and type formula = St.formula and type proof = St.proof) = struct
 
-  open St
   module Proof = Res.Make(L)(St)
 
+  open St
+
   exception Sat
   exception Unsat
   exception Restart
@@ -144,6 +145,24 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
     tatoms_qhead = 0;
   }
 
+  (* Iteration over subterms *)
+  module Mi = Map.Make(struct type t = int let compare = Pervasives.compare end)
+  let iter_map = ref Mi.empty
+
+  let iter_sub f v =
+    try
+      List.iter f (Mi.find v.vid !iter_map)
+    with Not_found ->
+      let l = ref [] in
+      Th.iter_assignable (fun t -> l := add_term t :: !l) v.pa.lit;
+      iter_map := Mi.add v.vid !l !iter_map;
+      List.iter f !l
+
+  let atom lit =
+    let res = add_atom lit in
+    iter_sub ignore res.var;
+    res
+
   (* Misc functions *)
   let to_float i = float_of_int i
   let to_int f = int_of_float f
@@ -620,7 +639,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
 
   (* Propagation (boolean and theory) *)
   let new_atom f =
-    let a = add_atom f in
+    let a = atom f in
     L.debug 10 "New atom : %a" St.pp_atom a;
     ignore (th_eval a);
     a
@@ -636,7 +655,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
     add_clause (fresh_tname ()) atoms (Lemma lemma)
 
   let slice_propagate f lvl =
-    let a = add_atom f in
+    let a = atom f in
     Iheap.grow_to_by_double env.order (St.nb_elt ());
     enqueue_bool a lvl (Semantic lvl)
 
@@ -877,7 +896,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
     add_clauses ?tag cnf
 
   let assume ?tag cnf =
-    let cnf = List.rev_map (List.rev_map St.add_atom) cnf in
+    let cnf = List.rev_map (List.rev_map atom) cnf in
     init_solver ?tag cnf
 
   let eval lit =
diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml
index a1956de9..9ebf753e 100644
--- a/solver/mcsolver.ml
+++ b/solver/mcsolver.ml
@@ -5,9 +5,9 @@ Copyright 2014 Simon Cruanes
 *)
 
 module Make (L : Log_intf.S)(E : Expr_intf.S)
-    (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t) = struct
+    (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t and type proof = E.proof) = struct
 
-  module St = Solver_types.McMake(L)(E)(Th)
+  module St = Solver_types.McMake(L)(E)
 
   module M = Internal.Make(L)(St)(Th)
 
diff --git a/solver/mcsolver.mli b/solver/mcsolver.mli
index d7f8b5d3..33672b3d 100644
--- a/solver/mcsolver.mli
+++ b/solver/mcsolver.mli
@@ -5,7 +5,7 @@ Copyright 2014 Simon Cruanes
 *)
 
 module Make (L : Log_intf.S)(E : Expr_intf.S)
-    (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t) : sig
+    (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t and type proof = E.proof) : sig
   (** Functor to create a solver parametrised by the atomic formulas and a theory. *)
 
   exception Unsat
@@ -13,7 +13,6 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
   module St : Solver_types.S
     with type term = E.Term.t
      and type formula = E.Formula.t
-     and type proof = Th.proof
 
   module Proof : Res.S
     with type atom = St.atom
diff --git a/solver/plugin_intf.ml b/solver/plugin_intf.ml
index d14fcba9..c2675822 100644
--- a/solver/plugin_intf.ml
+++ b/solver/plugin_intf.ml
@@ -82,10 +82,5 @@ module type S = sig
   (** Called at the end of the search in case a model has been found. If no new clause is
       pushed, then 'sat' is returned, else search is resumed. *)
 
-  val proof_debug : proof -> string * (formula list) * (term list) * (string option)
-  (** Returns debugging information on a proof, as a triplet consisting of
-      a name/identification string associated with the proof, arguments of the proof,
-      and an optional color for the proof background *)
-
 end
 
diff --git a/solver/res.ml b/solver/res.ml
index 79a9823a..0d0f6d61 100644
--- a/solver/res.ml
+++ b/solver/res.ml
@@ -294,105 +294,5 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
     Stack.push (Enter p) s;
     fold_aux s h f acc
 
-  (* Dot proof printing *)
-  module Dot = struct
-    let _i = ref 0
-    let new_id () = incr _i; "id_" ^ (string_of_int !_i)
-
-    let ids : (clause, (bool * string)) Hashtbl.t = Hashtbl.create 1007;;
-    let c_id c =
-      try
-        snd (Hashtbl.find ids c)
-      with Not_found ->
-        let id = new_id () in
-        Hashtbl.add ids c (false, id);
-        id
-
-    let clear_ids () =
-      Hashtbl.iter (fun c (_, id) -> Hashtbl.replace ids c (false, id)) ids
-
-    let is_drawn c =
-      ignore (c_id c);
-      fst (Hashtbl.find ids c)
-
-    let has_drawn c =
-      if not (is_drawn c) then
-        let b, id = Hashtbl.find ids c in
-        Hashtbl.replace ids c (true, id)
-      else
-        ()
-
-    let print_dot_rule opt f arg fmt cl =
-      Format.fprintf fmt "%s [shape=plaintext, label=<<TABLE %s %s>%a</TABLE>>];@\n"
-        (c_id cl) "BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\"" opt f arg
-
-    let print_dot_edge id_c fmt id_d =
-      Format.fprintf fmt "%s -> %s;@\n" id_c id_d
-
-    let print_res_atom id fmt a =
-      Format.fprintf fmt "%s [label=\"%a\"]" id St.print_atom a
-
-    let print_res_node concl p1 p2 fmt atom =
-      let id = new_id () in
-      Format.fprintf fmt "%a;@\n%a%a%a"
-        (print_res_atom id) atom
-        (print_dot_edge (c_id concl)) id
-        (print_dot_edge id) (c_id p1)
-        (print_dot_edge id) (c_id p2)
-
-    let color s = match s.[0] with
-      | 'E' -> "BGCOLOR=\"GREEN\""
-      | 'L' -> "BGCOLOR=\"GREEN\""
-      | _ -> "BGCOLOR=\"GREY\""
-
-    let rec print_dot_proof fmt p =
-      if not (is_drawn p.conclusion) then begin
-        has_drawn p.conclusion;
-        match p.step with
-        | Hypothesis ->
-          let aux fmt () =
-            Format.fprintf fmt "<TR><TD colspan=\"2\">%a</TD></TR><TR><TD>Hypothesis</TD><TD>%s</TD></TR>"
-              print_clause p.conclusion St.(p.conclusion.name)
-          in
-          print_dot_rule "BGCOLOR=\"LIGHTBLUE\"" aux () fmt p.conclusion
-        | Lemma proof ->
-          let name, f_args, t_args, color = St.proof_debug proof in
-          let color = match color with None -> "YELLOW" | Some c -> c in
-          let aux fmt () =
-            Format.fprintf fmt "<TR><TD colspan=\"2\">%a</TD></TR><TR><TD BGCOLOR=\"%s\" rowspan=\"%d\">%s</TD>"
-              print_clause p.conclusion color (max (List.length f_args + List.length t_args) 1) name;
-            if f_args <> [] then
-              Format.fprintf fmt "<TD>%a</TD></TR>%a%a" St.print_atom (List.hd f_args)
-                (fun fmt -> List.iter (fun a -> Format.fprintf fmt "<TR><TD>%a</TD></TR>" St.print_atom a)) (List.tl f_args)
-                (fun fmt -> List.iter (fun v -> Format.fprintf fmt "<TR><TD>%a</TD></TR>" St.print_lit v)) t_args
-            else if t_args <> [] then
-              Format.fprintf fmt "<TD>%a</TD></TR>%a" St.print_lit (List.hd t_args)
-                (fun fmt -> List.iter (fun v -> Format.fprintf fmt "<TR><TD>%a</TD></TR>" St.print_lit v)) (List.tl t_args)
-            else
-              Format.fprintf fmt "<TD></TD></TR>"
-          in
-          print_dot_rule "BGCOLOR=\"LIGHTBLUE\"" aux () fmt p.conclusion
-        | Resolution (proof1, proof2, a) ->
-          let aux fmt () =
-            Format.fprintf fmt "<TR><TD colspan=\"2\">%a</TD></TR><TR><TD>%s</TD><TD>%s</TD></TR>"
-              print_clause p.conclusion
-              "Resolution" St.(p.conclusion.name)
-          in
-          let p1 = expand proof1 in
-          let p2 = expand proof2 in
-          Format.fprintf fmt "%a%a%a%a"
-            (print_dot_rule (color p.conclusion.St.name) aux ()) p.conclusion
-            (print_res_node p.conclusion p1.conclusion p2.conclusion) a
-            print_dot_proof p1
-            print_dot_proof p2
-      end
-
-    let print fmt proof =
-      clear_ids ();
-      Format.fprintf fmt "digraph proof {@\n%a@\n}@." print_dot_proof (expand proof)
-  end
-
-  let print_dot = Dot.print
-
 end
 
diff --git a/solver/res_intf.ml b/solver/res_intf.ml
index 7334cdc4..d81628be 100644
--- a/solver/res_intf.ml
+++ b/solver/res_intf.ml
@@ -80,11 +80,8 @@ module type S = sig
   val unsat_core : proof -> clause list
   (** Returns the unsat_core of the given proof, i.e the lists of conclusions of all leafs of the proof. *)
 
-  val print_dot : Format.formatter -> proof -> unit
-  (** Print the given proof in dot format on the given formatter.
-      @deprecated use the Dot backend module instead. *)
-
   (** {3 Misc} *)
+
   val print_clause : Format.formatter -> clause -> unit
   (** A nice looking printer for clauses, which sort the atoms before printing. *)
 
diff --git a/solver/solver.ml b/solver/solver.ml
index 890b1178..b8f2bb5f 100644
--- a/solver/solver.ml
+++ b/solver/solver.ml
@@ -11,13 +11,7 @@
 (**************************************************************************)
 
 module Make (L : Log_intf.S)(E : Formula_intf.S)
-    (Th : Theory_intf.S with type formula = E.t) = struct
-
-  module Expr = struct
-    module Term = E
-    module Formula = E
-    include E
-  end
+    (Th : Theory_intf.S with type formula = E.t and type proof = E.proof) = struct
 
   module Plugin = struct
     type term = E.t
@@ -76,7 +70,7 @@ module Make (L : Log_intf.S)(E : Formula_intf.S)
     let proof_debug _ = assert false
   end
 
-  module St = Solver_types.SatMake(L)(E)(Th)
+  module St = Solver_types.SatMake(L)(E)
 
   module S = Internal.Make(L)(St)(Plugin)
 
diff --git a/solver/solver.mli b/solver/solver.mli
index 53e88b3d..6777f73e 100644
--- a/solver/solver.mli
+++ b/solver/solver.mli
@@ -12,7 +12,7 @@
 (**************************************************************************)
 
 module Make (L : Log_intf.S)(F : Formula_intf.S)
-    (Th : Theory_intf.S with type formula = F.t) : sig
+    (Th : Theory_intf.S with type formula = F.t and type proof = F.proof) : sig
   (** Functor to create a SMT Solver parametrised by the atomic
       formulas and a theory. *)
 
@@ -20,7 +20,7 @@ module Make (L : Log_intf.S)(F : Formula_intf.S)
 
   module St : Solver_types.S
     with type formula = F.t
-     and type proof = Th.proof
+     and type proof = F.proof
 
   module Proof : Res.S
     with type atom = St.atom
diff --git a/solver/solver_types.ml b/solver/solver_types.ml
index 4e45a7e6..9d363ed8 100644
--- a/solver/solver_types.ml
+++ b/solver/solver_types.ml
@@ -15,21 +15,14 @@ open Printf
 
 module type S = Solver_types_intf.S
 
-
 (* Solver types for McSat Solving *)
 (* ************************************************************************ *)
 
-module McMake (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
-    type formula = E.Formula.t and type term = E.Term.t) = struct
-
-  (* Flag for Mcsat v.s Pure Sat *)
-  let mcsat = true
-
-  (* Types declarations *)
+module McMake (L : Log_intf.S)(E : Expr_intf.S) = struct
 
   type term = E.Term.t
   type formula = E.Formula.t
-  type proof = Th.proof
+  type proof = E.proof
 
   type lit = {
     lid : int;
@@ -73,8 +66,11 @@ module McMake (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
     | Bcp of clause option
 
   and premise =
-    | History of clause list
     | Lemma of proof
+    | History of clause list
+
+  (* Flag for Mcsat v.s Pure Sat *)
+  let mcsat = true
 
   type elt = (lit, var) Either.t
 
@@ -172,7 +168,7 @@ module McMake (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
         MF.add f_map lit var;
         incr cpt_mk_var;
         Vec.push vars (Either.mk_right var);
-        Th.iter_assignable (fun t -> ignore (make_semantic_var t)) lit;
+        (* Th.iter_assignable (fun t -> ignore (make_semantic_var t)) lit; *)
         var, negated
 
   let add_term t = make_semantic_var t
@@ -209,7 +205,7 @@ module McMake (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
   let get_elt_id = function
     | Either.Left l -> l.lid | Either.Right v ->  v.vid
   let get_elt_level = function
-    | Either.Left (l :lit) -> l.level | Either.Right v ->  v.level
+    | Either.Left (l : lit) -> l.level | Either.Right v ->  v.level
   let get_elt_weight = function
     | Either.Left (l : lit) -> l.weight | Either.Right v ->  v.weight
 
@@ -235,24 +231,6 @@ module McMake (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
     let cpt = ref 0 in
     fun () -> incr cpt; "C" ^ (string_of_int !cpt)
 
-  (* Iteration over subterms *)
-  module Mi = Map.Make(struct type t = int let compare= Pervasives.compare end)
-  let iter_map = ref Mi.empty
-
-  let iter_sub f v =
-    try
-      List.iter f (Mi.find v.vid !iter_map)
-    with Not_found ->
-      let l = ref [] in
-      Th.iter_assignable (fun t -> l := add_term t :: !l) v.pa.lit;
-      iter_map := Mi.add v.vid !l !iter_map;
-      List.iter f !l
-
-  (* Proof debug info *)
-  let proof_debug p =
-    let name, l, l', color = Th.proof_debug p in
-    name, (List.map add_atom l), (List.map add_term l'), color
-
   (* Pretty printing for atoms and clauses *)
   let print_lit fmt v = E.Term.print fmt v.term
 
@@ -317,23 +295,14 @@ module McMake (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
 end
 
 
-
 (* Solver types for pure SAT Solving *)
 (* ************************************************************************ *)
 
-
-
-module SatMake (L : Log_intf.S)(E : Formula_intf.S)
-    (Th : Theory_intf.S with type formula = E.t ) = struct
-
-  (* Flag for Mcsat v.s Pure Sat *)
-  let mcsat = false
-
-  (* Types declarations *)
+module SatMake (L : Log_intf.S)(E : Formula_intf.S) = struct
 
   type term = E.t
   type formula = E.t
-  type proof = Th.proof
+  type proof = E.proof
 
   type lit = {
     lid : int;
@@ -377,9 +346,14 @@ module SatMake (L : Log_intf.S)(E : Formula_intf.S)
     | Bcp of clause option
 
   and premise =
-    | History of clause list
     | Lemma of proof
+    | History of clause list
 
+  (* Flag for Mcsat v.s Pure Sat *)
+  (* Flag for Mcsat v.s Pure Sat *)
+  let mcsat = false
+
+  (* Types declarations *)
   type elt = var
 
   (* Dummy values *)
diff --git a/solver/solver_types.mli b/solver/solver_types.mli
index a0eb10c6..9508254e 100644
--- a/solver/solver_types.mli
+++ b/solver/solver_types.mli
@@ -16,14 +16,12 @@ module type S = Solver_types_intf.S
 module McMake :
   functor (L : Log_intf.S) ->
   functor (E : Expr_intf.S) ->
-  functor (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t) ->
-    S with type term = E.Term.t and type formula = E.Formula.t and type proof = Th.proof
+    S with type term = E.Term.t and type formula = E.Formula.t and type proof = E.proof
 (** Functor to instantiate the types of clauses for a solver. *)
 
 module SatMake :
   functor (L : Log_intf.S) ->
   functor (E : Formula_intf.S) ->
-  functor (Th : Theory_intf.S with type formula = E.t) ->
-    S with type term = E.t and type formula = E.t and type proof = Th.proof
+    S with type term = E.t and type formula = E.t and type proof = E.proof
 (** Functor to instantiate the types of clauses for a solver. *)
 
diff --git a/solver/solver_types_intf.ml b/solver/solver_types_intf.ml
index fd1c506a..12bbfd76 100644
--- a/solver/solver_types_intf.ml
+++ b/solver/solver_types_intf.ml
@@ -64,8 +64,8 @@ module type S = sig
     | Bcp of clause option
 
   and premise =
-    | History of clause list
     | Lemma of proof
+    | History of clause list
 
   (** {2 Decisions and propagations} *)
   type t
@@ -113,10 +113,6 @@ module type S = sig
   (** Returns the variable linked with the given formula, and wether the atom associated with the formula
       is [var.pa] or [var.na] *)
 
-  val iter_sub : (lit -> unit) -> var -> unit
-  (** Iterates over the semantic var corresponding to subterms of the fiven literal, according
-      to Th.iter_assignable *)
-
   val empty_clause : clause
   (** The empty clause *)
   val make_clause : ?tag:int -> string -> atom list -> int -> bool -> premise -> clause
@@ -130,9 +126,6 @@ module type S = sig
   val fresh_hname : unit -> string
   (** Fresh names for clauses *)
 
-  val proof_debug : proof -> string * (atom list) * (lit list) * (string option)
-  (** Debugging info for proofs (see Plugin_intf). *)
-
   (** {2 Printing} *)
 
   val print_lit : Format.formatter -> lit -> unit