[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`

1 files changed, 3 insertions, 3 deletions

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 564c0965b..f0e41d27c 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."))