Module Ltac_plugin.Tactic_option
val declare_tactic_option : ?default:Tacexpr.glob_tactic_expr -> string -> (Vernacexpr.locality_flag -> Tacexpr.glob_tactic_expr -> unit) * (unit -> Vernacexpr.locality_flag * unit Proofview.tactic) * (unit -> Pp.t)