diff --git a/src/backend/dot.ml b/src/backend/dot.ml
index fdfec48f..0ef710c1 100644
--- a/src/backend/dot.ml
+++ b/src/backend/dot.ml
@@ -101,5 +101,9 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom and type lemma := S.lemm
 
 end
 
-
+module Simple(S : Res.S)(A : Arg with type atom := S.St.formula and type lemma := S.lemma) =
+  Make(S)(struct
+    let lemma_info = A.lemma_info
+    let print_atom fmt a = A.print_atom fmt a.S.St.lit
+  end)
 
diff --git a/src/backend/dot.mli b/src/backend/dot.mli
index d47271a2..5e47032b 100644
--- a/src/backend/dot.mli
+++ b/src/backend/dot.mli
@@ -48,3 +48,7 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom and type lemma := S.lemm
   S with type t := S.proof
 (** Functor for making a module to export proofs to the DOT format. *)
 
+module Simple(S : Res.S)(A : Arg with type atom := S.St.formula and type lemma := S.lemma) :
+  S with type t := S.proof
+(** Functor for making a module to export proofs to the DOT format. *)
+