Tactic.Tele
include Tactic
type tac
val update_span : Basis.LexingUtil.span option -> tac -> tac
val whnf : tac -> tac
val rule : ?name:string -> S.tele RM.m -> tac
val run : tac -> S.tele RM.m