-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
+
+(* Warning: this tactic has no effect on the proof term.
+ It just changes the name of an hypothesis in the current sequent *)
+val rename: from:string -> to_:string -> ProofEngineTypes.tactic
+
+ (* change the current goal to those referred by the given meta number *)
+val set_goal: int -> ProofEngineTypes.tactic