package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

Module `Tactic_option`Source

Sourcetype tac_option_locality

Sourceval tac_option_locality : tac_option_locality Attributes.attribute

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

package rocq-runtime

Module Tactic_optionSource

Module `Tactic_option`Source