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`
---
 vernac/vernacentries.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 564c0965bd..f0e41d27cc 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -909,7 +909,7 @@ let vernac_set_used_variables e =
     if List.is_empty to_clear then (p, ())
     else
       let tac = Tactics.clear to_clear in
-      fst (Pfedit.solve SelectAll None tac p), ()
+      fst (Pfedit.solve Goal_select.SelectAll None tac p), ()
   end
 
 (*****************************)
@@ -1611,7 +1611,7 @@ let get_current_context_of_args = function
 
 let query_command_selector ?loc = function
   | None -> None
-  | Some (SelectNth n) -> Some n
+  | Some (Goal_select.SelectNth n) -> Some n
   | _ -> user_err ?loc ~hdr:"query_command_selector"
       (str "Query commands only support the single numbered goal selector.")
 
@@ -1911,7 +1911,7 @@ let vernac_subproof gln =
   Proof_global.simple_with_current_proof (fun _ p ->
     match gln with
     | None -> Proof.focus subproof_cond () 1 p
-    | Some (SelectNth n) -> Proof.focus subproof_cond () n p
+    | Some (Goal_select.SelectNth n) -> Proof.focus subproof_cond () n p
     | _ -> user_err ~hdr:"bracket_selector"
              (str "Brackets only support the single numbered goal selector."))
 
-- 
cgit v1.2.3