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