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 )