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