diff options
| author | Théo Zimmermann | 2018-05-02 15:04:57 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-05-02 15:04:57 +0200 |
| commit | fd146ca38202c9843b4240cbdac0ae75f57e4d67 (patch) | |
| tree | 39f0c957c4ea02e6976299b4183b6bcfa8ea9f7a /tactics | |
| parent | 48ec42bb91b8c0fb4d5930e62e29a408de594482 (diff) | |
| parent | fca82378cd2824534383f1f5bc09d08fade1dc17 (diff) | |
Merge PR #7339: [api] Move bullets and goals selectors to `proofs/`
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacticals.ml | 12 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 2 |
2 files changed, 7 insertions, 7 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 82b178388e..6c7db26c77 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -492,12 +492,12 @@ module New = struct Proofview.tclINDEPENDENT (Proofview.tclPROGRESS t) (* Select a subset of the goals *) - let tclSELECT = function - | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i - | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l - | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id - | Vernacexpr.SelectAll -> anomaly ~label:"tclSELECT" Pp.(str "SelectAll not allowed here") - | Vernacexpr.SelectAlreadyFocused -> + let tclSELECT = let open Goal_select in function + | SelectNth i -> Proofview.tclFOCUS i i + | SelectList l -> Proofview.tclFOCUSLIST l + | SelectId id -> Proofview.tclFOCUSID id + | SelectAll -> anomaly ~label:"tclSELECT" Pp.(str "SelectAll not allowed here") + | SelectAlreadyFocused -> anomaly ~label:"tclSELECT" Pp.(str "SelectAlreadyFocused not allowed here") (* Check that holes in arguments have been resolved *) diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 340d8fbf3d..bc2f60186a 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -223,7 +223,7 @@ module New : sig val tclCOMPLETE : 'a tactic -> 'a tactic val tclSOLVE : unit tactic list -> unit tactic val tclPROGRESS : unit tactic -> unit tactic - val tclSELECT : Vernacexpr.goal_selector -> 'a tactic -> 'a tactic + val tclSELECT : Goal_select.t -> 'a tactic -> 'a tactic val tclWITHHOLES : bool -> 'a tactic -> Evd.evar_map -> 'a tactic val tclDELAYEDWITHHOLES : bool -> 'a delayed_open -> ('a -> unit tactic) -> unit tactic |