module ProverSearch:sig
..end
val first : ProofEngine.tree ->
anchor:ProofEngine.node -> Strategy.t array -> ProofEngine.fork option
val backtrack : ProofEngine.tree ->
anchor:ProofEngine.node -> loop:bool -> ProofEngine.fork option