sig
  module Make :
    functor (Seq : Sigs.SEQUENT) ->
      sig
        type 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
end