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 : ?unknown:bool -> ProofEngine.tree -> unit
  type status = [ `Main | `Pending of int | `Proved ]
  type state = [ `Opened | `Pending of int | `Proved | `Script of int ]
  type current =
      [ `Internal of ProofEngine.node
      | `Leaf of int * ProofEngine.node
      | `Main ]
  type position = [ `Leaf of int | `Main | `Node of ProofEngine.node ]
  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_model : ProofEngine.tree -> Model.t
  val node_model : ProofEngine.node -> Model.t
  val opened : ProofEngine.node -> bool
  val proved : ProofEngine.node -> bool
  val title : ProofEngine.node -> string
  val state : ProofEngine.node -> ProofEngine.state
  val parent : ProofEngine.node -> ProofEngine.node option
  val pending : ProofEngine.node -> int
  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 :
    resolve:bool ->
    ProofEngine.fork -> ProofEngine.node * (string * ProofEngine.node) list
  val pretty : 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