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 = [ `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 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 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 :
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