package rocq-runtime

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

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