sig
  module Make :
    functor (Seq : Sigs.SEQUENT) (Defs : Sigs.DEFS) ->
      sig
        type abdrule_t = Abdrule.Make(Seq)(Defs).t
        type proof_t = Proof.Make(Seq).t
        type defs_t = Defs.t
        module Seq :
          sig
            type t = Seq.t
            val equal : t -> t -> bool
            val equal_upto_tags : t -> t -> bool
            val tags : t -> Tags.t
            val to_string : t -> string
            val to_melt : t -> Latex.t
            val pp : Format.formatter -> t -> unit
          end
        module Proof :
          sig
            type t = Proof.Make(Seq).t
            type seq_t = Seq.t
            type node_t = Proofnode.Make(Seq).t
            val mk : seq_t -> t
            val add_axiom : int -> string -> t -> t
            val add_backlink : int -> string -> int -> Tagpairs.t -> t -> t
            val add_inf :
              int ->
              string ->
              (seq_t * Tagpairs.t * Tagpairs.t) list -> t -> int list * t
            val add_subprf : t -> int -> t -> t
            val extract_subproof : int -> t -> t
            val find : int -> t -> node_t
            val get_seq : int -> t -> seq_t
            val size : t -> int
            val num_backlinks : t -> int
            val fresh_idx : t -> int
            val fresh_idxs : 'a list -> t -> int list
            val get_ancestry : int -> t -> (int * node_t) list
            val is_closed_at : t -> int -> bool
            val check : t -> bool
            val is_closed : t -> bool
            val to_list : t -> (int * node_t) list
            val pp : Format.formatter -> t -> unit
            val to_string : t -> string
            val to_melt : t -> Latex.t
          end
        val bfs :
          int ->
          abdrule_t ->
          Seq.t -> defs_t -> (defs_t -> bool) -> (proof_t * defs_t) option
        val print_proof_stats : Proof.t -> unit
        val melt_proof : out_channel -> Proof.t -> unit
      end
end