sig
  type t
  type seq_t
  type node_t
  val mk : Sigs.PROOF.seq_t -> Sigs.PROOF.t
  val add_axiom : int -> string -> Sigs.PROOF.t -> Sigs.PROOF.t
  val add_backlink :
    int -> string -> int -> Tagpairs.t -> Sigs.PROOF.t -> Sigs.PROOF.t
  val add_inf :
    int ->
    string ->
    (Sigs.PROOF.seq_t * Tagpairs.t * Tagpairs.t) list ->
    Sigs.PROOF.t -> int list * Sigs.PROOF.t
  val add_subprf : Sigs.PROOF.t -> int -> Sigs.PROOF.t -> Sigs.PROOF.t
  val extract_subproof : int -> Sigs.PROOF.t -> Sigs.PROOF.t
  val find : int -> Sigs.PROOF.t -> Sigs.PROOF.node_t
  val get_seq : int -> Sigs.PROOF.t -> Sigs.PROOF.seq_t
  val size : Sigs.PROOF.t -> int
  val num_backlinks : Sigs.PROOF.t -> int
  val fresh_idx : Sigs.PROOF.t -> int
  val fresh_idxs : 'a list -> Sigs.PROOF.t -> int list
  val get_ancestry : int -> Sigs.PROOF.t -> (int * Sigs.PROOF.node_t) list
  val is_closed_at : Sigs.PROOF.t -> int -> bool
  val check : Sigs.PROOF.t -> bool
  val is_closed : Sigs.PROOF.t -> bool
  val to_list : Sigs.PROOF.t -> (int * Sigs.PROOF.node_t) list
  val pp : Format.formatter -> Sigs.PROOF.t -> unit
  val to_string : Sigs.PROOF.t -> string
  val to_melt : Sigs.PROOF.t -> Latex.t
end