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