sig
  module type S = Backend_intf.S
  module type Arg =
    sig
      type hyp
      type lemma
      type assumption
      val prove_hyp : Format.formatter -> string -> Coq.Arg.hyp -> unit
      val prove_lemma : Format.formatter -> string -> Coq.Arg.lemma -> unit
      val prove_assumption :
        Format.formatter -> string -> Coq.Arg.assumption -> unit
    end
  module Make :
    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
  module Simple :
    functor
      (S : Res.S) (A : sig
                         type hyp = S.St.formula list
                         val prove_hyp :
                           Format.formatter -> string -> hyp -> unit
                         val prove_lemma :
                           Format.formatter -> string -> S.lemma -> unit
                         val prove_assumption :
                           Format.formatter -> string -> S.St.formula -> unit
                       end) ->
      sig val print : Format.formatter -> S.proof -> unit end
end