sig
  module Make :
    functor (Seq : Sigs.SEQUENT) ->
      sig
        type seq_t = Seq.t
        type proof_t = Proof.Make(Seq).t
        type axiom_f = seq_t -> string option
        type infrule_app = (seq_t * Tagpairs.t * Tagpairs.t) list * string
        type infrule_f = seq_t -> infrule_app list
        type backrule_f = seq_t -> seq_t -> (Tagpairs.t * string) list
        type select_f = int -> proof_t -> int list
        type t = int -> proof_t -> (int list * proof_t) Blist.t
        val mk_axiom : axiom_f -> t
        val mk_infrule : infrule_f -> t
        val mk_backrule : bool -> select_f -> backrule_f -> t
        val all_nodes : select_f
        val closed_nodes : select_f
        val ancestor_nodes : select_f
        val syntactically_equal_nodes : select_f
        val fail : t
        val identity : t
        val attempt : t -> t
        val compose : t -> t -> t
        val compose_pairwise : t -> t list -> t
        val choice : t list -> t
        val first : t list -> t
        val sequence : t list -> t
        val conditional : (seq_t -> bool) -> t -> t
        val combine_axioms : t -> t -> t
      end
end