functor
  (S : Res.S) (A : sig
                     val prove_hyp :
                       Format.formatter -> string -> S.clause -> unit
                     val prove_lemma :
                       Format.formatter -> string -> S.clause -> unit
                     val prove_assumption :
                       Format.formatter -> string -> S.clause -> unit
                   end) ->
  sig val print : Format.formatter -> S.proof -> unit end