sig
  module Make :
    functor (Seq : Sigs.SEQUENT) ->
      sig
        type rule_t = Proofrule.Make(Seq).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 last_search_depth : int ref
        val idfs : int -> int -> rule_t -> rule_t -> Seq.t -> Proof.t option
        val print_proof_stats : Proof.t -> unit
        val melt_proof : out_channel -> Proof.t -> unit
      end
end