+module type Status =
+ sig
+ type input_status
+ type output_status
+ type tactic
+ val id_tac : tactic
+ val mk_tactic : (input_status -> output_status) -> tactic
+ val apply_tactic : tactic -> input_status -> output_status
+ val goals : output_status -> ProofEngineTypes.goal list
+ val set_goals: output_status -> ProofEngineTypes.goal list -> output_status
+ val focus : output_status -> ProofEngineTypes.goal -> input_status
+ end