sig
  module Loc = Libzipperposition.ParseLocation
  type form = Libzipperposition.TypedSTerm.t
  type bool_lit = BBox.Lit.t
  type 'a sequence = ('a -> unit) -> unit
  val section : Libzipperposition.Util.Section.t
  type rule_info =
      I_subst of Libzipperposition.Substs.t
    | I_pos of Libzipperposition.Position.t
    | I_comment of string
  type rule = { rule_name : string; rule_info : ProofStep.rule_info list; }
  val mk_rule :
    ?subst:Libzipperposition.Substs.t list ->
    ?pos:Libzipperposition.Position.t list ->
    ?comment:string list -> string -> ProofStep.rule
  type kind =
      Inference of ProofStep.rule
    | Simplification of ProofStep.rule
    | Esa of ProofStep.rule
    | Assert of Libzipperposition.StatementSrc.t
    | Goal of Libzipperposition.StatementSrc.t
    | Data of Libzipperposition.StatementSrc.t *
        Libzipperposition.Type.t Libzipperposition.Statement.data
    | Trivial
  type result =
      Form of ProofStep.form
    | Clause of SClause.t
    | BoolClause of ProofStep.bool_lit list
  type t = private {
    id : int;
    kind : ProofStep.kind;
    dist_to_goal : int option;
    parents : ProofStep.of_ list;
  }
  and of_ = { step : ProofStep.t; result : ProofStep.result; }
  type proof = ProofStep.of_
  val result : ProofStep.of_ -> ProofStep.result
  val step : ProofStep.of_ -> ProofStep.t
  val kind : ProofStep.t -> ProofStep.kind
  val parents : ProofStep.t -> ProofStep.of_ list
  val compare_proof : ProofStep.of_ -> ProofStep.of_ -> int
  val equal_proof : ProofStep.of_ -> ProofStep.of_ -> bool
  val hash_proof : ProofStep.of_ -> int
  module PTbl :
    sig
      type key = of_
      type 'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val reset : 'a t -> unit
      val copy : 'a t -> 'a t
      val add : 'a t -> key -> 'a -> unit
      val remove : 'a t -> key -> unit
      val find : 'a t -> key -> 'a
      val find_all : 'a t -> key -> 'a list
      val replace : 'a t -> key -> 'a -> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val length : 'a t -> int
      val stats : 'a t -> Hashtbl.statistics
      val get : 'a t -> key -> 'a option
      val get_or : 'a t -> key -> or_:'a -> 'a
      val add_list : 'a list t -> key -> 'a -> unit
      val incr : ?by:int -> int t -> key -> unit
      val decr : ?by:int -> int t -> key -> unit
      val keys : 'a t -> key CCHashtbl.sequence
      val values : 'a t -> 'a CCHashtbl.sequence
      val keys_list : 'a t -> key list
      val values_list : 'a t -> 'a list
      val map_list : (key -> 'a -> 'b) -> 'a t -> 'b list
      val to_seq : 'a t -> (key * 'a) CCHashtbl.sequence
      val of_seq : (key * 'a) CCHashtbl.sequence -> 'a t
      val add_seq : 'a t -> (key * 'a) CCHashtbl.sequence -> unit
      val add_seq_count : int t -> key CCHashtbl.sequence -> unit
      val of_seq_count : key CCHashtbl.sequence -> int t
      val to_list : 'a t -> (key * 'a) list
      val of_list : (key * 'a) list -> 'a t
      val update : 'a t -> f:(key -> 'a option -> 'a option) -> k:key -> unit
      val print :
        key CCHashtbl.printer ->
        'a CCHashtbl.printer -> 'a t CCHashtbl.printer
    end
  val mk_trivial : ProofStep.t
  val mk_data :
    Libzipperposition.StatementSrc.t ->
    Libzipperposition.Type.t Libzipperposition.Statement.data -> ProofStep.t
  val mk_assert : Libzipperposition.StatementSrc.t -> ProofStep.t
  val mk_goal : Libzipperposition.StatementSrc.t -> ProofStep.t
  val mk_assert' :
    ?loc:Loc.t -> file:string -> name:string -> unit -> ProofStep.t
  val mk_goal' :
    ?loc:Loc.t -> file:string -> name:string -> unit -> ProofStep.t
  val mk_inference : rule:ProofStep.rule -> ProofStep.of_ list -> ProofStep.t
  val mk_simp : rule:ProofStep.rule -> ProofStep.of_ list -> ProofStep.t
  val mk_esa : rule:ProofStep.rule -> ProofStep.of_ list -> ProofStep.t
  val mk_f_trivial : ProofStep.form -> ProofStep.of_
  val mk_f_inference :
    rule:ProofStep.rule ->
    ProofStep.form -> ProofStep.of_ list -> ProofStep.of_
  val mk_f_simp :
    rule:ProofStep.rule ->
    ProofStep.form -> ProofStep.of_ list -> ProofStep.of_
  val mk_f_esa :
    rule:ProofStep.rule ->
    ProofStep.form -> ProofStep.of_ list -> ProofStep.of_
  val mk_c : ProofStep.t -> SClause.t -> ProofStep.of_
  val mk_bc : ProofStep.t -> ProofStep.bool_lit list -> ProofStep.of_
  val adapt_f : ProofStep.of_ -> ProofStep.form -> ProofStep.of_
  val adapt_c : ProofStep.of_ -> SClause.t -> ProofStep.of_
  val is_trivial : ProofStep.t -> bool
  val is_assert : ProofStep.t -> bool
  val is_goal : ProofStep.t -> bool
  val rule : ProofStep.t -> ProofStep.rule option
  val equal : ProofStep.t -> ProofStep.t -> bool
  val hash : ProofStep.t -> int
  val compare : ProofStep.t -> ProofStep.t -> int
  val compare_by_result : ProofStep.of_ -> ProofStep.of_ -> int
  val distance_to_goal : ProofStep.t -> int option
  val pp_rule : info:bool -> ProofStep.rule CCFormat.printer
  val pp_src : Libzipperposition.StatementSrc.t CCFormat.printer
  val pp_src_tstp : Libzipperposition.StatementSrc.t CCFormat.printer
  val pp_kind : ProofStep.kind CCFormat.printer
  val pp_kind_tstp : ProofStep.kind CCFormat.printer
end