Tactic.Syn
include Tactic
type tac
val update_span : Basis.LexingUtil.span option -> tac -> tac
val whnf : tac -> tac
val rule : ?name:string -> (S.t * D.tp) RM.m -> tac
val run : tac -> (S.t * D.tp) RM.m
val ann : Chk.tac -> Tp.tac -> tac
val catch : tac -> (exn -> tac) -> tac