val mk_tactic : (input_status -> output_status) -> tactic
val apply_tactic : tactic -> input_status -> output_status
+ val get_status: input_status -> ProofEngineTypes.status
+ val get_proof: output_status -> ProofEngineTypes.proof
val goals : output_status -> goal list * goal list (** opened, closed goals *)
val set_goals: goal list * goal list -> output_status -> output_status
val get_stack : input_status -> Stack.t