From fca82378cd2824534383f1f5bc09d08fade1dc17 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 24 Apr 2018 18:21:49 +0200 Subject: [api] Move bullets and goals selectors to `proofs/` `Vernacexpr` lives conceptually higher than `proof`, however, datatypes for bullets and goal selectors are in `Vernacexpr`. In particular, we move: - `proof_bullet`: to `Proof_bullet` - `goal_selector`: to a new file `Goal_select` --- tactics/tacticals.ml | 12 ++++++------ tactics/tacticals.mli | 2 +- 2 files changed, 7 insertions(+), 7 deletions(-) (limited to 'tactics') diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 82b178388..6c7db26c7 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 340d8fbf3..bc2f60186 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 -- cgit v1.2.3