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