[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, 6 insertions, 5 deletions

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 83c875707..89117caf4 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -145,7 +145,7 @@ open Pputils
         | SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
 
   let pr_search a gopt b pr_p =
-    pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt
+    pr_opt (fun g -> Goal_select.pr_goal_selector g ++ str ":"++ spc()) gopt
     ++
       match a with
       | SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b
@@ -508,7 +508,7 @@ open Pputils
     | PrintVisibility s ->
       keyword "Print Visibility" ++ pr_opt str s
     | PrintAbout (qid,l,gopt) ->
-       pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt
+       pr_opt (fun g -> Goal_select.pr_goal_selector g ++ str ":"++ spc()) gopt
        ++ keyword "About" ++ spc()  ++ pr_smart_global qid ++ pr_univ_name_list l
     | PrintImplicit qid ->
       keyword "Print Implicit" ++ spc()  ++ pr_smart_global qid
@@ -1122,7 +1122,7 @@ open Pputils
           | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c)
         in
         let pr_i = match io with None -> mt ()
-                               | Some i -> Proof_bullet.pr_goal_selector i ++ str ": " in
+                               | Some i -> Goal_select.pr_goal_selector i ++ str ": " in
         return (pr_i ++ pr_mayeval r c)
       | VernacGlobalCheck c ->
         return (hov 2 (keyword "Type" ++ pr_constrarg c))
@@ -1176,7 +1176,8 @@ open Pputils
       | VernacProofMode s ->
         return (keyword "Proof Mode" ++ str s)
       | VernacBullet b ->
-        return (begin match b with
+        (* XXX: Redundant with Proof_bullet.print *)
+        return (let open Proof_bullet in begin match b with
           | Dash n -> str (String.make n '-')
           | Star n -> str (String.make n '*')
           | Plus n -> str (String.make n '+')
@@ -1184,7 +1185,7 @@ open Pputils
       | VernacSubproof None ->
         return (str "{")
       | VernacSubproof (Some i) ->
-        return (Proof_bullet.pr_goal_selector i ++ str ":" ++ spc () ++ str "{")
+        return (Goal_select.pr_goal_selector i ++ str ":" ++ spc () ++ str "{")
       | VernacEndSubproof ->
         return (str "}")