[proof] Move bullets to their own module.

Bullets were placed inside the `Proof_global` module, I guess that due
to the global registration function. However, it has logically nothing
to do with the functionality of `Proof_global` and the current
placement may create some interference between the developers
reworking proof state handling and bullets.

We thus put the bullet functionality into its own, independent file.

11 files changed, 323 insertions, 313 deletions

diff --git a/API/API.ml b/API/API.ml
index 2b7bbd561..85e8f2e73 100644
--- a/API/API.ml
+++ b/API/API.ml
@@ -79,6 +79,7 @@ module Nametab = Nametab
 module Vernacentries = Vernacentries
 module Mltop = Mltop
 module Goal = Goal
+module Proof_bullet = Proof_bullet
 module Proof_global = Proof_global
 module Proof = Proof
 module Smartlocate = Smartlocate
diff --git a/API/API.mli b/API/API.mli
index d844e8bf5..61da0c605 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -3376,6 +3376,11 @@ sig
   end
 end
 
+module Proof_bullet :
+sig
+  val get_default_goal_selector : unit -> Vernacexpr.goal_selector
+end
+
 module Proof_global :
 sig
   type proof_mode = Proof_global.proof_mode = {
@@ -3410,7 +3415,6 @@ sig
     (unit Proofview.tactic -> Proof.proof -> Proof.proof) -> unit
   val compact_the_proof : unit -> unit
   val register_proof_mode : proof_mode -> unit
-  val get_default_goal_selector : unit -> Vernacexpr.goal_selector
 
   exception NoCurrentProof
   val give_me_the_proof : unit -> Proof.proof
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 7855fbcfc..ebeb2d913 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -433,7 +433,7 @@ let is_explicit_terminator = function TacSolve _ -> true | _ -> false
 VERNAC tactic_mode EXTEND VernacSolve
 | [ - ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
     [ classify_as_proofstep ] -> [
-    let g = Option.default (Proof_global.get_default_goal_selector ()) g in
+    let g = Option.default (Proof_bullet.get_default_goal_selector ()) g in
     vernac_solve g n t def
   ]
 | [ - "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 781af4789..ca1499bc2 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -105,7 +105,7 @@ open Decl_kinds
         | 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_global.pr_goal_selector g ++ str ":"++ spc()) gopt
+    pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt
     ++
       match a with
       | SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b
@@ -490,7 +490,7 @@ open Decl_kinds
     | PrintVisibility s ->
       keyword "Print Visibility" ++ pr_opt str s
     | PrintAbout (qid,gopt) ->
-       pr_opt (fun g -> Proof_global.pr_goal_selector g ++ str ":"++ spc()) gopt
+       pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt
        ++ keyword "About" ++ spc()  ++ pr_smart_global qid
     | PrintImplicit qid ->
       keyword "Print Implicit" ++ spc()  ++ pr_smart_global qid
@@ -1130,7 +1130,7 @@ open Decl_kinds
           | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c)
         in
         let pr_i = match io with None -> mt ()
-                               | Some i -> Proof_global.pr_goal_selector i ++ str ": " in
+                               | Some i -> Proof_bullet.pr_goal_selector i ++ str ": " in
         return (pr_i ++ pr_mayeval r c)
       | VernacGlobalCheck c ->
         return (hov 2 (keyword "Type" ++ pr_constrarg c))
diff --git a/printing/printer.ml b/printing/printer.ml
index 3c31dd96b..58cfc2b88 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -798,7 +798,7 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
 	  | _ , _, _ ->
             let end_cmd =
               str "This subproof is complete, but there are some unfocused goals." ++
-              (let s = Proof_global.Bullet.suggest p in
+              (let s = Proof_bullet.suggest p in
                if Pp.ismt s then s else fnl () ++ s) ++
               fnl ()
             in
diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml
new file mode 100644
index 000000000..f80cb7cc6
--- /dev/null
+++ b/proofs/proof_bullet.ml
@@ -0,0 +1,248 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Proof
+
+type t = Vernacexpr.bullet
+
+let bullet_eq b1 b2 = match b1, b2 with
+| Vernacexpr.Dash n1, Vernacexpr.Dash n2 -> n1 = n2
+| Vernacexpr.Star n1, Vernacexpr.Star n2 -> n1 = n2
+| Vernacexpr.Plus n1, Vernacexpr.Plus n2 -> n1 = n2
+| _ -> false
+
+let pr_bullet b =
+  match b with
+  | Vernacexpr.Dash n -> Pp.(str (String.make n '-'))
+  | Vernacexpr.Star n -> Pp.(str (String.make n '*'))
+  | Vernacexpr.Plus n -> Pp.(str (String.make n '+'))
+
+
+type behavior = {
+  name : string;
+  put : proof -> t -> proof;
+  suggest: proof -> Pp.t
+}
+
+let behaviors = Hashtbl.create 4
+let register_behavior b = Hashtbl.add behaviors b.name b
+
+(*** initial modes ***)
+let none = {
+  name = "None";
+  put = (fun x _ -> x);
+  suggest = (fun _ -> Pp.mt ())
+}
+let _ = register_behavior none
+
+module Strict = struct
+  type suggestion =
+  | Suggest of t (* this bullet is mandatory here *)
+  | Unfinished of t (* no mandatory bullet here, but this bullet is unfinished *)
+  | NoBulletInUse (* No mandatory bullet (or brace) here, no bullet pending,
+      	       some focused goals exists. *)
+  | NeedClosingBrace (* Some unfocussed goal exists "{" needed to focus them *)
+  | ProofFinished (* No more goal anywhere *)
+
+  (* give a message only if more informative than the standard coq message *)
+  let suggest_on_solved_goal sugg =
+    match sugg with
+    | NeedClosingBrace -> Pp.(str"Try unfocusing with \"}\".")
+    | NoBulletInUse -> Pp.mt ()
+    | ProofFinished -> Pp.mt ()
+    | Suggest b -> Pp.(str"Focus next goal with bullet " ++ pr_bullet b ++ str".")
+    | Unfinished b -> Pp.(str"The current bullet " ++ pr_bullet b ++ str" is unfinished.")
+
+  (* give always a message. *)
+  let suggest_on_error sugg =
+    match sugg with
+    | NeedClosingBrace -> Pp.(str"Try unfocusing with \"}\".")
+    | NoBulletInUse -> assert false (* This should never raise an error. *)
+    | ProofFinished -> Pp.(str"No more subgoals.")
+    | Suggest b -> Pp.(str"Expecting " ++ pr_bullet b ++ str".")
+    | Unfinished b -> Pp.(str"Current bullet " ++ pr_bullet b ++ str" is not finished.")
+
+  exception FailedBullet of t * suggestion
+
+  let _ =
+    CErrors.register_handler
+      (function
+      | FailedBullet (b,sugg) ->
+        let prefix = Pp.(str"Wrong bullet " ++ pr_bullet b ++ str": ") in
+        CErrors.user_err ~hdr:"Focus" Pp.(prefix ++ suggest_on_error sugg)
+      | _ -> raise CErrors.Unhandled)
+
+
+  (* spiwack: we need only one focus kind as we keep a stack of (distinct!) bullets *)
+  let bullet_kind = (new_focus_kind () : t list focus_kind)
+  let bullet_cond = done_cond ~loose_end:true bullet_kind
+
+  (* spiwack: as it is bullets are reset (locally) by *any* non-bullet focusing command
+     experience will tell if this is the right discipline of if we want to be finer and
+     reset them only for a choice of bullets. *)
+  let get_bullets pr =
+    if is_last_focus bullet_kind pr then
+      get_at_focus bullet_kind pr
+    else
+      []
+
+  let has_bullet bul pr =
+    let rec has_bullet = function
+      | b'::_ when bullet_eq bul b' -> true
+      | _::l -> has_bullet l
+      | [] -> false
+    in
+    has_bullet (get_bullets pr)
+
+  (* pop a bullet from proof [pr]. There should be at least one
+     bullet in use. If pop impossible (pending proofs on this level
+     of bullet or higher) then raise [Proof.CannotUnfocusThisWay]. *)
+  let pop pr =
+    match get_bullets pr with
+    | b::_ -> unfocus bullet_kind pr () , b
+    | _ -> assert false
+
+  let push (b:t) pr =
+    focus bullet_cond (b::get_bullets pr) 1 pr
+
+  (* Used only in the next function.
+     TODO: use a recursive function instead? *)
+  exception SuggestFound of t
+
+  let suggest_bullet (prf : proof): suggestion =
+    if is_done prf then ProofFinished
+    else if not (no_focused_goal prf)
+    then (* No suggestion if a bullet is not mandatory, look for an unfinished bullet *)
+      match get_bullets prf with
+      | b::_ -> Unfinished b
+      | _ -> NoBulletInUse
+    else (* There is no goal under focus but some are unfocussed,
+            let us look at the bullet needed. If no  *)
+      let pcobaye = ref prf in
+      try
+        while true do
+          let pcobaye', b = pop !pcobaye in
+         (* pop went well, this means that there are no more goals
+          *under this* bullet b, see if a new b can be pushed. *)
+          (try let _ = push b pcobaye' in (* push didn't fail so a new b can be pushed. *)
+      	 raise (SuggestFound b)
+           with SuggestFound _ as e -> raise e
+           | _ -> ()); (* b could not be pushed, so we must look for a outer bullet *)
+          pcobaye := pcobaye'
+        done;
+        assert false
+      with SuggestFound b -> Suggest b
+      | _ -> NeedClosingBrace (* No push was possible, but there are still
+      			   subgoals somewhere: there must be a "}" to use. *)
+
+
+  let rec pop_until (prf : proof) bul : proof =
+    let prf', b = pop prf in
+    if bullet_eq bul b then prf'
+    else pop_until prf' bul
+
+  let put p bul =
+    try
+      if not (has_bullet bul p) then
+        (* bullet is not in use, so pushing it is always ok unless
+           no goal under focus. *)
+        push bul p
+      else
+        match suggest_bullet p with
+        | Suggest suggested_bullet when bullet_eq bul suggested_bullet
+            -> (* suggested_bullet is mandatory and you gave the right one *)
+          let p' = pop_until p bul in
+          push bul p'
+      (* the bullet you gave is in use but not the right one *)
+        | sugg -> raise (FailedBullet (bul,sugg))
+    with NoSuchGoals _ -> (* push went bad *)
+      raise (FailedBullet (bul,suggest_bullet p))
+
+  let strict = {
+    name = "Strict Subproofs";
+    put = put;
+    suggest = (fun prf -> suggest_on_solved_goal (suggest_bullet prf))
+
+  }
+  let _ = register_behavior strict
+end
+
+(* Current bullet behavior, controlled by the option *)
+let current_behavior = ref Strict.strict
+
+let _ =
+  Goptions.(declare_string_option {
+    optdepr = false;
+    optname = "bullet behavior";
+    optkey = ["Bullet";"Behavior"];
+    optread = begin fun () ->
+      (!current_behavior).name
+    end;
+    optwrite = begin fun n ->
+      current_behavior :=
+        try Hashtbl.find behaviors n
+        with Not_found ->
+          CErrors.user_err Pp.(str ("Unknown bullet behavior: \"" ^ n ^ "\"."))
+    end
+  })
+
+let put p b =
+  (!current_behavior).put p b
+
+let suggest p =
+  (!current_behavior).suggest p
+
+(**********************************************************)
+(*                                                        *)
+(*                     Default goal selector              *)
+(*                                                        *)
+(**********************************************************)
+
+
+(* Default goal selector: selector chosen when a tactic is applied
+   without an explicit selector. *)
+let default_goal_selector = ref (Vernacexpr.SelectNth 1)
+let get_default_goal_selector () = !default_goal_selector
+
+let pr_range_selector (i, j) =
+  if i = j then Pp.int i
+  else Pp.(int i ++ str "-" ++ int j)
+
+let pr_goal_selector = function
+  | Vernacexpr.SelectAll -> Pp.str "all"
+  | Vernacexpr.SelectNth i -> Pp.int i
+  | Vernacexpr.SelectList l ->
+    Pp.(str "["
+     ++ prlist_with_sep pr_comma pr_range_selector l
+     ++ str "]")
+  | Vernacexpr.SelectId id -> Names.Id.print id
+
+let parse_goal_selector = function
+  | "all" -> Vernacexpr.SelectAll
+  | i ->
+      let err_msg = "The default selector must be \"all\" or a natural number." in
+      begin try
+              let i = int_of_string i in
+              if i < 0 then CErrors.user_err Pp.(str err_msg);
+              Vernacexpr.SelectNth i
+        with Failure _ -> CErrors.user_err Pp.(str err_msg)
+      end
+
+let _ =
+  Goptions.(declare_string_option{optdepr = false;
+                                  optname = "default goal selector" ;
+                                  optkey = ["Default";"Goal";"Selector"] ;
+                                  optread = begin fun () ->
+                                            Pp.string_of_ppcmds
+                                              (pr_goal_selector !default_goal_selector)
+                                            end;
+                                  optwrite = begin fun n ->
+                                    default_goal_selector := parse_goal_selector n
+                                  end
+                                 })
+
diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli
new file mode 100644
index 000000000..9ae521d3f
--- /dev/null
+++ b/proofs/proof_bullet.mli
@@ -0,0 +1,53 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(**********************************************************)
+(*                                                        *)
+(*                                 Bullets                *)
+(*                                                        *)
+(**********************************************************)
+
+open Proof
+
+type t = Vernacexpr.bullet
+
+(** A [behavior] is the data of a put function which
+    is called when a bullet prefixes a tactic, a suggest function
+    suggesting the right bullet to use on a given proof, together
+    with a name to identify the behavior. *)
+type behavior = {
+  name : string;
+  put : proof -> t -> proof;
+  suggest: proof -> Pp.t
+}
+
+(** A registered behavior can then be accessed in Coq
+    through the command [Set Bullet Behavior "name"].
+
+    Two modes are registered originally:
+    * "Strict Subproofs":
+      - If this bullet follows another one of its kind, defocuses then focuses
+        (which fails if the focused subproof is not complete).
+      - If it is the first bullet of its kind, then focuses a new subproof.
+    * "None": bullets don't do anything *)
+val register_behavior : behavior -> unit
+
+(** Handles focusing/defocusing with bullets:
+     *)
+val put : proof -> t -> proof
+val suggest : proof -> Pp.t
+
+(**********************************************************)
+(*                                                        *)
+(*                     Default goal selector              *)
+(*                                                        *)
+(**********************************************************)
+
+val pr_goal_selector : Vernacexpr.goal_selector -> Pp.std_ppcmds
+val get_default_goal_selector : unit -> Vernacexpr.goal_selector
+
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 5ec34a638..d8d3a9027 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -447,265 +447,6 @@ let set_terminator hook =
   | [] -> raise NoCurrentProof
   | p :: ps -> pstates := { p with terminator = CEphemeron.create hook } :: ps
 
-
-
-
-(**********************************************************)
-(*                                                        *)
-(*                                 Bullets                *)
-(*                                                        *)
-(**********************************************************)
-
-module Bullet = struct
-
-  type t = Vernacexpr.bullet
-
-  let bullet_eq b1 b2 = match b1, b2 with
-  | Vernacexpr.Dash n1, Vernacexpr.Dash n2 -> n1 = n2
-  | Vernacexpr.Star n1, Vernacexpr.Star n2 -> n1 = n2
-  | Vernacexpr.Plus n1, Vernacexpr.Plus n2 -> n1 = n2
-  | _ -> false
-
-  let pr_bullet b =
-    match b with
-    | Vernacexpr.Dash n -> str (String.make n '-')
-    | Vernacexpr.Star n -> str (String.make n '*')
-    | Vernacexpr.Plus n -> str (String.make n '+')
-
-
-  type behavior = {
-    name : string;
-    put : Proof.proof -> t -> Proof.proof;
-    suggest: Proof.proof -> std_ppcmds
-  }
-
-  let behaviors = Hashtbl.create 4
-  let register_behavior b = Hashtbl.add behaviors b.name b
-
-  (*** initial modes ***)
-  let none = {
-    name = "None";
-    put = (fun x _ -> x);
-    suggest = (fun _ -> mt ())
-  }
-  let _ = register_behavior none
-
-  module Strict = struct
-    type suggestion =
-    | Suggest of t (* this bullet is mandatory here *)
-    | Unfinished of t (* no mandatory bullet here, but this bullet is unfinished *)
-    | NoBulletInUse (* No mandatory bullet (or brace) here, no bullet pending,
-		       some focused goals exists. *)
-    | NeedClosingBrace (* Some unfocussed goal exists "{" needed to focus them *)
-    | ProofFinished (* No more goal anywhere *)
-
-    (* give a message only if more informative than the standard coq message *)
-    let suggest_on_solved_goal sugg =
-      match sugg with
-      | NeedClosingBrace -> str"Try unfocusing with \"}\"."
-      | NoBulletInUse -> mt ()
-      | ProofFinished -> mt ()
-      | Suggest b -> str"Focus next goal with bullet " ++ pr_bullet b ++ str"."
-      | Unfinished b -> str"The current bullet " ++ pr_bullet b ++ str" is unfinished."
-
-    (* give always a message. *)
-    let suggest_on_error sugg =
-      match sugg with
-      | NeedClosingBrace -> str"Try unfocusing with \"}\"."
-      | NoBulletInUse -> assert false (* This should never raise an error. *)
-      | ProofFinished -> str"No more subgoals."
-      | Suggest b -> str"Expecting " ++ pr_bullet b ++ str"."
-      | Unfinished b -> str"Current bullet " ++ pr_bullet b ++ str" is not finished."
-
-    exception FailedBullet of t * suggestion
-
-    let _ =
-      CErrors.register_handler
-	(function
-	| FailedBullet (b,sugg) ->
-	  let prefix = str"Wrong bullet " ++ pr_bullet b ++ str": " in
-	  CErrors.user_err ~hdr:"Focus" (prefix ++ suggest_on_error sugg)
-	| _ -> raise CErrors.Unhandled)
-
-
-    (* spiwack: we need only one focus kind as we keep a stack of (distinct!) bullets *)
-    let bullet_kind = (Proof.new_focus_kind () : t list Proof.focus_kind)
-    let bullet_cond = Proof.done_cond ~loose_end:true bullet_kind
-
-    (* spiwack: as it is bullets are reset (locally) by *any* non-bullet focusing command
-       experience will tell if this is the right discipline of if we want to be finer and
-       reset them only for a choice of bullets. *)
-    let get_bullets pr =
-      if Proof.is_last_focus bullet_kind pr then
-	Proof.get_at_focus bullet_kind pr
-      else
-	[]
-
-    let has_bullet bul pr =
-      let rec has_bullet = function
-	| b'::_ when bullet_eq bul b' -> true
-	| _::l -> has_bullet l
-	| [] -> false
-      in
-      has_bullet (get_bullets pr)
-
-    (* pop a bullet from proof [pr]. There should be at least one
-       bullet in use. If pop impossible (pending proofs on this level
-       of bullet or higher) then raise [Proof.CannotUnfocusThisWay]. *)
-    let pop pr =
-      match get_bullets pr with
-      | b::_ -> Proof.unfocus bullet_kind pr () , b
-      | _ -> assert false
-
-    let push (b:t) pr =
-      Proof.focus bullet_cond (b::get_bullets pr) 1 pr
-
-    (* Used only in the next function.
-       TODO: use a recursive function instead? *)
-    exception SuggestFound of t
-
-    let suggest_bullet (prf:Proof.proof): suggestion =
-      if Proof.is_done prf then ProofFinished
-      else if not (Proof.no_focused_goal prf)
-      then (* No suggestion if a bullet is not mandatory, look for an unfinished bullet *)
-	match get_bullets prf with
-	| b::_ -> Unfinished b
-	| _ -> NoBulletInUse
-      else (* There is no goal under focus but some are unfocussed,
-	      let us look at the bullet needed. If no  *)
-	let pcobaye = ref prf in
-	try
-	  while true do
-	    let pcobaye', b = pop !pcobaye in
-	   (* pop went well, this means that there are no more goals
-	    *under this* bullet b, see if a new b can be pushed. *)
-	    (try let _ = push b pcobaye' in (* push didn't fail so a new b can be pushed. *)
-		 raise (SuggestFound b)
-	     with SuggestFound _ as e -> raise e
-	     | _ -> ()); (* b could not be pushed, so we must look for a outer bullet *)
-	    pcobaye := pcobaye'
-	  done;
-	  assert false
-	with SuggestFound b -> Suggest b
-	| _ -> NeedClosingBrace (* No push was possible, but there are still
-				   subgoals somewhere: there must be a "}" to use. *)
-
-
-    let rec pop_until (prf:Proof.proof) bul: Proof.proof =
-      let prf', b = pop prf in
-      if bullet_eq bul b then prf'
-      else pop_until prf' bul
-
-    let put p bul =
-      try
-	if not (has_bullet bul p) then
-	  (* bullet is not in use, so pushing it is always ok unless
-	     no goal under focus. *)
-	  push bul p
-	else
-	  match suggest_bullet p with
-	  | Suggest suggested_bullet when bullet_eq bul suggested_bullet
-	      -> (* suggested_bullet is mandatory and you gave the right one *)
-	    let p' = pop_until p bul in
-	    push bul p'
-	(* the bullet you gave is in use but not the right one *)
-	  | sugg -> raise (FailedBullet (bul,sugg))
-      with Proof.NoSuchGoals _ -> (* push went bad *)
-	raise (FailedBullet (bul,suggest_bullet p))
-
-    let strict = {
-      name = "Strict Subproofs";
-      put = put;
-      suggest = (fun prf -> suggest_on_solved_goal (suggest_bullet prf))
-
-    }
-    let _ = register_behavior strict
-  end
-
-  (* Current bullet behavior, controlled by the option *)
-  let current_behavior = ref Strict.strict
-
-  let _ =
-    Goptions.(declare_string_option {
-      optdepr = false;
-      optname = "bullet behavior";
-      optkey = ["Bullet";"Behavior"];
-      optread = begin fun () ->
-	(!current_behavior).name
-      end;
-      optwrite = begin fun n ->
-	current_behavior :=
-          try Hashtbl.find behaviors n
-          with Not_found ->
-            CErrors.user_err Pp.(str ("Unknown bullet behavior: \"" ^ n ^ "\"."))
-      end
-    })
-
-  let put p b =
-    (!current_behavior).put p b
-
-  let suggest p =
-    (!current_behavior).suggest p
-end
-
-
-let _ =
-  let hook n =
-    let prf = give_me_the_proof () in
-    (Bullet.suggest prf) in
-  Proofview.set_nosuchgoals_hook hook
-
-
-(**********************************************************)
-(*                                                        *)
-(*                     Default goal selector              *)
-(*                                                        *)
-(**********************************************************)
-
-
-(* Default goal selector: selector chosen when a tactic is applied
-   without an explicit selector. *)
-let default_goal_selector = ref (Vernacexpr.SelectNth 1)
-let get_default_goal_selector () = !default_goal_selector
-
-let pr_range_selector (i, j) =
-  if i = j then int i
-  else int i ++ str "-" ++ int j
-
-let pr_goal_selector = function
-  | Vernacexpr.SelectAll -> str "all"
-  | Vernacexpr.SelectNth i -> int i
-  | Vernacexpr.SelectList l ->
-     str "["
-     ++ prlist_with_sep pr_comma pr_range_selector l
-     ++ str "]"
-  | Vernacexpr.SelectId id -> Id.print id
-
-let parse_goal_selector = function
-  | "all" -> Vernacexpr.SelectAll
-  | i ->
-      let err_msg = "The default selector must be \"all\" or a natural number." in
-      begin try
-              let i = int_of_string i in
-              if i < 0 then CErrors.user_err Pp.(str err_msg);
-              Vernacexpr.SelectNth i
-        with Failure _ -> CErrors.user_err Pp.(str err_msg)
-      end
-
-let _ =
-  Goptions.(declare_string_option{optdepr = false;
-                                  optname = "default goal selector" ;
-                                  optkey = ["Default";"Goal";"Selector"] ;
-                                  optread = begin fun () ->
-                                            string_of_ppcmds
-                                              (pr_goal_selector !default_goal_selector)
-                                            end;
-                                  optwrite = begin fun n ->
-                                    default_goal_selector := parse_goal_selector n
-                                  end
-                                 })
-
-
 module V82 = struct
   let get_current_initial_conclusions () =
   let { pid; strength; proof } = cur_pstate () in
@@ -734,3 +475,11 @@ let update_global_env () =
        let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in
        let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac p in
          (p, ())))
+
+(* XXX: Bullet hook, should be really moved elsewhere *)
+let _ =
+  let hook n =
+    let prf = give_me_the_proof () in
+    (Proof_bullet.suggest prf) in
+  Proofview.set_nosuchgoals_hook hook
+
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 22cc8cf59..bb9d66b6e 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -121,52 +121,6 @@ val get_used_variables : unit -> Context.Named.t option
 
 val get_universe_binders : unit -> universe_binders option
 
-(**********************************************************)
-(*                                                        *)
-(*                                 Bullets                *)
-(*                                                        *)
-(**********************************************************)
-
-module Bullet : sig
-  type t = Vernacexpr.bullet
-
-  (** A [behavior] is the data of a put function which
-      is called when a bullet prefixes a tactic, a suggest function
-      suggesting the right bullet to use on a given proof, together
-      with a name to identify the behavior. *)
-  type behavior = {
-    name : string;
-    put : Proof.proof -> t -> Proof.proof;
-    suggest: Proof.proof -> Pp.std_ppcmds
-  }
-
-  (** A registered behavior can then be accessed in Coq
-      through the command [Set Bullet Behavior "name"].
-
-      Two modes are registered originally:
-      * "Strict Subproofs":
-        - If this bullet follows another one of its kind, defocuses then focuses
-          (which fails if the focused subproof is not complete).
-        - If it is the first bullet of its kind, then focuses a new subproof.
-      * "None": bullets don't do anything *)
-  val register_behavior : behavior -> unit
-
-  (** Handles focusing/defocusing with bullets:
-       *)
-  val put : Proof.proof -> t -> Proof.proof
-  val suggest : Proof.proof -> Pp.std_ppcmds
-end
-
-
-(**********************************************************)
-(*                                                        *)
-(*                     Default goal selector              *)
-(*                                                        *)
-(**********************************************************)
-
-val pr_goal_selector : Vernacexpr.goal_selector -> Pp.std_ppcmds
-val get_default_goal_selector : unit -> Vernacexpr.goal_selector
-
 module V82 : sig
   val get_current_initial_conclusions : unit -> Names.Id.t *(EConstr.types list *
   Decl_kinds.goal_kind)
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 804a54360..0ea2bd66b 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -5,6 +5,7 @@ Proof_using
 Logic
 Refine
 Proof
+Proof_bullet
 Proof_global
 Redexpr
 Refiner
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ef16df5b7..b2466631f 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1830,9 +1830,9 @@ let vernac_end_subproof () =
   Proof_global.simple_with_current_proof (fun _ p ->
     Proof.unfocus subproof_kind p ())
 
-let vernac_bullet (bullet:Proof_global.Bullet.t) =
+let vernac_bullet (bullet : Proof_bullet.t) =
   Proof_global.simple_with_current_proof (fun _ p ->
-    Proof_global.Bullet.put p bullet)
+    Proof_bullet.put p bullet)
 
 let vernac_show = let open Feedback in function
   | ShowScript -> assert false  (* Only the stm knows the script *)