package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
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)