functor
  (S : Res.S) (A : sig
                     type hyp = S.St.formula list
                     type assumption = S.St.formula
                     val print_atom :
                       Format.formatter -> S.St.formula -> unit
                     val hyp_info :
                       hyp ->
                       string * string option *
                       (Format.formatter -> unit -> unit) list
                     val lemma_info :
                       S.lemma ->
                       string * string option *
                       (Format.formatter -> unit -> unit) list
                     val assumption_info :
                       assumption ->
                       string * string option *
                       (Format.formatter -> unit -> unit) list
                   end) ->
  sig val print : Format.formatter -> S.proof -> unit end