package rocq-runtime

  1. Overview
  2. Docs
package rocq-runtime
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Tactic_optionSource

Sourcetype tac_option_locality
Sourceval 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)