diff --git a/src/backend/coq.ml b/src/backend/coq.ml
index c8915000..43f618b8 100644
--- a/src/backend/coq.ml
+++ b/src/backend/coq.ml
@@ -32,7 +32,6 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
     end)
 
   let name c = c.S.St.name
-  let name_tmp c = c.S.St.name ^ "_tmp"
 
   let pp_atom fmt a =
     if a == S.St.(a.var.pa) then
@@ -60,12 +59,6 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
     in
     aux M.empty c.S.St.atoms 0
 
-  let clausify fmt clause =
-    Format.fprintf fmt "(* Encoding theory clause %s into: %s *)@\n"
-      (name_tmp clause) (name clause);
-    Format.fprintf fmt "assert (%s: %a).@\ntauto. clear %s.@\n"
-      (name clause) pp_clause clause (name_tmp clause)
-
   let clause_iter m format fmt clause =
     let aux atom = Format.fprintf fmt format (M.find atom m) in
     Array.iter aux clause.S.St.atoms
@@ -121,14 +114,11 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
     let clause = node.S.conclusion in
     match node.S.step with
     | S.Hypothesis ->
-      A.prove_hyp fmt (name_tmp clause) clause;
-      clausify fmt clause
+      A.prove_hyp fmt (name clause) clause
     | S.Assumption ->
-      A.prove_assumption fmt (name_tmp clause) clause;
-      clausify fmt clause
+      A.prove_assumption fmt (name clause) clause
     | S.Lemma _ ->
-      A.prove_lemma fmt (name_tmp clause) clause;
-      clausify fmt clause
+      A.prove_lemma fmt (name clause) clause
     | S.Duplicate (p, l) ->
       let c = (S.expand p).S.conclusion in
       elim_duplicate fmt clause c l
diff --git a/src/backend/coq.mli b/src/backend/coq.mli
index 76faabfc..9d26b806 100644
--- a/src/backend/coq.mli
+++ b/src/backend/coq.mli
@@ -31,7 +31,11 @@ module type Arg = sig
   val prove_assumption : Format.formatter -> string -> assumption -> unit
   (** Proving function for hypotheses, lemmas and assumptions.
       [prove_x fmt name x] should prove [x], and be such that after
-      executing it, [x] is among the coq hypotheses under the name [name]. *)
+      executing it, [x] is among the coq hypotheses under the name [name].
+      The hypothesis should be the encoding of the given clause, i.e
+      for a clause [a \/ not b \/ c], the proved hypothesis should be:
+      [ ~ a -> ~ ~ b -> ~ c -> False ], keeping the same order as the
+      one in the atoms array of the clause. *)
 
 end