* http://cs.unibo.it/helm/.
*)
-val clearbody: hyp: Cic.hypothesis -> ProofEngineTypes.tactic
-val clear: hyp: Cic.hypothesis -> ProofEngineTypes.tactic
+val clearbody: hyp:string -> ProofEngineTypes.tactic
+val clear: hyp:string -> ProofEngineTypes.tactic
+
+ (* change the current goal to those referred by the given meta number *)
+val set_goal: int -> ProofEngineTypes.tactic