sig
  type tree
  type node
  val get : Wpo.t -> [ `None | `Proof | `Saved | `Script ]
  val proof : main:Wpo.t -> ProofEngine.tree
  val reset : ProofEngine.tree -> unit
  val remove : Wpo.t -> unit
  val validate : ?incomplete:bool -> ProofEngine.tree -> unit
  type status =
      [ `Invalid
      | `Passed
      | `Pending of int
      | `Proved
      | `StillResist of int
      | `Unproved ]
  type current =
      [ `Internal of ProofEngine.node
      | `Leaf of int * ProofEngine.node
      | `Main ]
  type position = [ `Leaf of int | `Main | `Node of ProofEngine.node ]
  val pool : ProofEngine.tree -> Lang.F.pool
  val saved : ProofEngine.tree -> bool
  val set_saved : ProofEngine.tree -> bool -> unit
  val status : ProofEngine.tree -> ProofEngine.status
  val current : ProofEngine.tree -> ProofEngine.current
  val goto : ProofEngine.tree -> ProofEngine.position -> unit
  val main : ProofEngine.tree -> Wpo.t
  val head : ProofEngine.tree -> Wpo.t
  val goal : ProofEngine.node -> Wpo.t
  val tree_context : ProofEngine.tree -> WpContext.t
  val node_context : ProofEngine.node -> WpContext.t
  val title : ProofEngine.node -> string
  val proved : ProofEngine.node -> bool
  val pending : ProofEngine.node -> int
  val parent : ProofEngine.node -> ProofEngine.node option
  val children : ProofEngine.node -> (string * ProofEngine.node) list
  val tactical : ProofEngine.node -> ProofScript.jtactic option
  val get_strategies : ProofEngine.node -> int * Strategy.t array
  val set_strategies :
    ProofEngine.node -> ?index:int -> Strategy.t array -> unit
  val forward : ProofEngine.tree -> unit
  val cancel : ProofEngine.tree -> unit
  type fork
  val anchor :
    ProofEngine.tree -> ?node:ProofEngine.node -> unit -> ProofEngine.node
  val fork :
    ProofEngine.tree ->
    anchor:ProofEngine.node ->
    ProofScript.jtactic -> Tactical.process -> ProofEngine.fork
  val iter : (Wpo.t -> unit) -> ProofEngine.fork -> unit
  val commit :
    ProofEngine.fork -> ProofEngine.node * (string * ProofEngine.node) list
  val pretty : Stdlib.Format.formatter -> ProofEngine.fork -> unit
  val script : ProofEngine.tree -> ProofScript.jscript
  val bind : ProofEngine.node -> ProofScript.jscript -> unit
  val bound : ProofEngine.node -> ProofScript.jscript
end