package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

Module `Ltac_plugin.Tactic_option`Source

Sourcetype tac_option_locality

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

package rocq-runtime

Module Ltac_plugin.Tactic_optionSource

Module `Ltac_plugin.Tactic_option`Source