package rocq-runtime

  1. Overview
  2. Docs

Module Goal_selectSource

Sourcetype t =
  1. | SelectAlreadyFocused
  2. | SelectList of Proofview.goal_range_selector list
  3. | SelectAll
Sourceval select_nth : int -> t
Sourceval pr_goal_selector : t -> Pp.t
Sourceval get_default_goal_selector : unit -> t
Sourceval tclSELECT : ?nosuchgoal:'a Proofview.tactic -> t -> 'a Proofview.tactic -> 'a Proofview.tactic