type t = proofval hash : t -> intmodule Tbl : CCHashtbl.S with type key = tIn all the following constructors, theories defaults to the empty list. Axiom constructors have default role "axiom"
val is_proof_of_false : t -> boolval as_graph : (t, rule * Subst.Projection.t option * infos) CCGraph.tGet a graph of the proof
val pp_result_of : t CCFormat.printerval pp_notrec : t CCFormat.printerNon recursive printing on formatter
val pp_notrec1 : t CCFormat.printerNon recursive printing on formatter, including parents
val pp_tstp : t CCFormat.printerval pp_normal : t CCFormat.printerval pp_zf : t CCFormat.printerval pp_in : Options.print_format -> t CCFormat.printerPrints the proof according to the given input switch
val pp_dot : name:string -> t CCFormat.printerPretty print the proof as a DOT graph
val pp_dot_file : ?name:string -> string -> t -> unitprint to dot into a file
val pp_dot_seq : name:string -> t Iter.t CCFormat.printerPrint a set of proofs as a DOT graph, sharing common subproofs
val pp_dot_seq_file : ?name:string -> string -> t Iter.t -> unitsame as pp_dot_seq but into a file