Tactic_option
val tac_option_locality : tac_option_locality Attributes.attribute
val declare_tactic_option : ?default:Gentactic.glob_generic_tactic -> string -> (?loc:Loc.t ->
tac_option_locality -> Gentactic.glob_generic_tactic -> unit) * (unit -> unit Proofview.tactic) * (unit -> Pp.t)