diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-24 18:21:49 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-01 01:22:00 +0200 |
| commit | fca82378cd2824534383f1f5bc09d08fade1dc17 (patch) | |
| tree | fe95ef8dff5e0e47cb80a54d913fd2a0c8f97ce3 /tactics | |
| parent | 8f477d20f6c933537d80bd838b04d13042a12011 (diff) | |
[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`
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 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 |