diff --git a/.merlin b/.merlin
index 2354e067..86bc450d 100644
--- a/.merlin
+++ b/.merlin
@@ -1,12 +1,14 @@
 S sat
 S smt
 S solver
-S util
 S backend
+S util
+S util/smtlib
 
 B _build/
 B _build/sat
 B _build/smt
 B _build/solver
 B _build/util
+B _build/smtlib
 B _build/backend
diff --git a/backend/dedukti.ml b/backend/dedukti.ml
index 2bd18c80..218aca9b 100644
--- a/backend/dedukti.ml
+++ b/backend/dedukti.ml
@@ -16,7 +16,7 @@ module type Arg = sig
   val context : Format.formatter -> proof -> unit
 end
 
-module Make(S : Res.S)(A : Arg with type formula := S.St.formula and type proof := S.proof) = struct
+module Make(S : Res.S)(A : Arg with type formula := S.St.formula and type lemma := S.lemma and type proof := S.proof) = struct
 
   let pp_nl fmt = Format.fprintf fmt "@\n"
   let fprintf fmt format = Format.kfprintf pp_nl fmt format
diff --git a/backend/dedukti.mli b/backend/dedukti.mli
index b39aa26a..be352eb3 100644
--- a/backend/dedukti.mli
+++ b/backend/dedukti.mli
@@ -14,6 +14,9 @@ end
 
 module Make :
   functor(S : Res.S) ->
-  functor(A : Arg with type formula := S.St.formula and type proof := S.proof) ->
+  functor(A : Arg
+          with type formula := S.St.formula
+           and type lemma := S.lemma
+           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/main.ml b/main.ml
index 1fef2a70..2a879b0d 100644
--- a/main.ml
+++ b/main.ml
@@ -22,6 +22,7 @@ type sat_input =
 
 type sat_output =
   | Standard (* Only output problem status *)
+  | Dedukti
   | Dot
 
 type solver =
@@ -39,6 +40,7 @@ let input_list = [
 ]
 let output_list = [
   "dot", Dot;
+  "dk", Dedukti;
 ]
 let solver_list = [
   "smt", Smt;
@@ -96,14 +98,19 @@ let print format = match !output with
   | Dot ->
     Format.fprintf std "/* ";
     Format.kfprintf (fun fmt -> Format.fprintf fmt " */@.") std format
+  | Dedukti ->
+    Format.fprintf std "(; ";
+    Format.kfprintf (fun fmt -> Format.fprintf fmt " ;)@.") std format
 
 let print_proof proof = match !output with
   | Standard -> ()
-  | Dot -> Smt.print_proof std proof
+  | Dot -> Smt.print_dot std proof
+  | Dedulti -> Smt.print_dedukti std proof
 
 let print_mcproof proof = match !output with
   | Standard -> ()
-  | Dot -> Mcsat.print_proof std proof
+  | Dot -> Mcsat.print_dot std proof
+  | Dedulti -> Mcsat.print_dedukti std proof
 
 let rec print_cl fmt = function
   | [] -> Format.fprintf fmt "[]"
@@ -121,15 +128,15 @@ let print_mclause l =
 
 let print_cnf cnf = match !output with
   | Standard -> print_lcl cnf
-  | Dot -> ()
+  | Dot | Dedukti -> ()
 
 let print_unsat_core u = match !output with
   | Standard -> print_lclause u
-  | Dot -> ()
+  | Dot | Dedukti -> ()
 
 let print_mc_unsat_core u = match !output with
   | Standard -> print_mclause u
-  | Dot -> ()
+  | Dot | Dedukti -> ()
 
 (* Arguments parsing *)
 let file = ref ""
diff --git a/smt/smt.ml b/smt/smt.ml
index 4052b468..27bbe374 100644
--- a/smt/smt.ml
+++ b/smt/smt.ml
@@ -67,8 +67,14 @@ module Make(Dummy:sig end) = struct
       let print_atom = St.print_atom
       let lemma_info () = "Proof", Some "PURPLE", []
     end)
+  module Dedukti = Dedukti.Make(Proof)(struct
+      let print _ _ = ()
+      let prove _ _ = ()
+      let context _ _ = ()
+    end)
 
   let print_clause = St.print_clause
-  let print_proof = Dot.print
+  let print_dot = Dot.print
+  let print_dedulti = Dedukti.print
 
 end
diff --git a/smt/smt.mli b/smt/smt.mli
index f11e3865..f703efe4 100644
--- a/smt/smt.mli
+++ b/smt/smt.mli
@@ -12,7 +12,10 @@ module Make(Dummy: sig end) : sig
   val print_clause : Format.formatter -> St.clause -> unit
   (** Print the clause on the given formatter. *)
 
-  val print_proof : Format.formatter -> Proof.proof -> unit
+  val print_dot : Format.formatter -> Proof.proof -> unit
+  (** Print the given proof in dot format. *)
+
+  val print_dedukti : Format.formatter -> Proof.proof -> unit
   (** Print the given proof in dot format. *)
 
 end