Module Ltac_plugin.Tactic_option

type tac_option_locality
val tac_option_locality : tac_option_locality Attributes.attribute
val declare_tactic_option : ?default:Tacexpr.glob_tactic_expr -> string -> (?loc:Loc.t -> tac_option_locality -> Tacexpr.glob_tactic_expr -> unit) * (unit -> unit Proofview.tactic) * (unit -> Pp.t)