Refiner.Hole
val silent_hole : string option -> Tactic.Chk.tac
val unleash_hole : string option -> Tactic.Chk.tac
val silent_syn_hole : string option -> Tactic.Syn.tac
val unleash_syn_hole : string option -> Tactic.Syn.tac