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

8 files changed, 125 insertions, 76 deletions

diff --git a/proofs/goal_select.ml b/proofs/goal_select.ml
new file mode 100644
index 000000000..65a94a2c6
--- /dev/null
+++ b/proofs/goal_select.ml
@@ -0,0 +1,68 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Names
+
+(* spiwack: I'm choosing, for now, to have [goal_selector] be a
+   different type than [goal_reference] mostly because if it makes sense
+   to print a goal that is out of focus (or already solved) it doesn't
+   make sense to apply a tactic to it. Hence it the types may look very
+   similar, they do not seem to mean the same thing. *)
+type t =
+  | SelectAlreadyFocused
+  | SelectNth of int
+  | SelectList of (int * int) list
+  | SelectId of Id.t
+  | SelectAll
+
+(* Default goal selector: selector chosen when a tactic is applied
+   without an explicit selector. *)
+let default_goal_selector = ref (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
+  | SelectAlreadyFocused -> Pp.str "!"
+  | SelectAll -> Pp.str "all"
+  | SelectNth i -> Pp.int i
+  | SelectList l ->
+    Pp.(str "["
+     ++ prlist_with_sep pr_comma pr_range_selector l
+     ++ str "]")
+  | SelectId id -> Names.Id.print id
+
+let parse_goal_selector = function
+  | "!" -> SelectAlreadyFocused
+  | "all" -> 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);
+              SelectNth i
+        with Failure _ -> CErrors.user_err Pp.(str err_msg)
+      end
+
+let _ = let open Goptions in
+  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/goal_select.mli b/proofs/goal_select.mli
new file mode 100644
index 000000000..b1c572388
--- /dev/null
+++ b/proofs/goal_select.mli
@@ -0,0 +1,26 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Names
+
+(* spiwack: I'm choosing, for now, to have [goal_selector] be a
+   different type than [goal_reference] mostly because if it makes sense
+   to print a goal that is out of focus (or already solved) it doesn't
+   make sense to apply a tactic to it. Hence it the types may look very
+   similar, they do not seem to mean the same thing. *)
+type t =
+  | SelectAlreadyFocused
+  | SelectNth of int
+  | SelectList of (int * int) list
+  | SelectId of Id.t
+  | SelectAll
+
+val pr_goal_selector : t -> Pp.t
+val get_default_goal_selector : unit -> t
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 62a38fa32..03c0969fa 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -100,8 +100,8 @@ let solve ?with_end_tac gi info_lvl tac pr =
       | None -> tac
       | Some _ -> Proofview.Trace.record_info_trace tac
     in
-    let tac = match gi with
-      | Vernacexpr.SelectAlreadyFocused ->
+    let tac = let open Goal_select in match gi with
+      | SelectAlreadyFocused ->
         let open Proofview.Notations in
         Proofview.numgoals >>= fun n ->
         if n == 1 then tac
@@ -113,10 +113,10 @@ let solve ?with_end_tac gi info_lvl tac pr =
           in
           Proofview.tclZERO e
 
-      | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i tac
-      | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l tac
-      | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id tac
-      | Vernacexpr.SelectAll -> tac
+      | SelectNth i -> Proofview.tclFOCUS i i tac
+      | SelectList l -> Proofview.tclFOCUSLIST l tac
+      | SelectId id -> Proofview.tclFOCUSID id tac
+      | SelectAll -> tac
     in
     let tac =
       if use_unification_heuristics () then
@@ -133,7 +133,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
   with
     Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof")
 
-let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac)
+let by tac = Proof_global.with_current_proof (fun _ -> solve (Goal_select.SelectNth 1) None tac)
 
 let instantiate_nth_evar_com n com = 
   Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.instantiate_evar n com p)
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 65cde3a3a..805635dfa 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -75,7 +75,7 @@ val current_proof_statement :
     tac] applies [tac] to all subgoals. *)
 
 val solve : ?with_end_tac:unit Proofview.tactic ->
-      Vernacexpr.goal_selector -> int option -> unit Proofview.tactic ->
+      Goal_select.t -> int option -> unit Proofview.tactic ->
       Proof.t -> Proof.t * bool
 
 (** [by tac] applies tactic [tac] to the 1st subgoal of the current
diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml
index d6f7c0e93..cc3e79f85 100644
--- a/proofs/proof_bullet.ml
+++ b/proofs/proof_bullet.ml
@@ -10,19 +10,22 @@
 
 open Proof
 
-type t = Vernacexpr.bullet
+type t =
+    | Dash of int
+    | Star of int
+    | Plus of int
 
 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
+| Dash n1, Dash n2 -> n1 = n2
+| Star n1, Star n2 -> n1 = n2
+| Plus n1, 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 '+'))
+  | Dash n -> Pp.(str (String.make n '-'))
+  | Star n -> Pp.(str (String.make n '*'))
+  | Plus n -> Pp.(str (String.make n '+'))
 
 
 type behavior = {
@@ -195,54 +198,5 @@ let 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.SelectAlreadyFocused -> Pp.str "!"
-  | 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
-  | "!" -> Vernacexpr.SelectAlreadyFocused
-  | "all" -> Vernacexpr.SelectAll
-  | i ->
-      let err_msg = "The default selector must be \"all\" or \"!\" 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
-                                 })
-
+let pr_goal_selector = Goal_select.pr_goal_selector
+let get_default_goal_selector = Goal_select.get_default_goal_selector
diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli
index ffbaa0fac..a09a7ec1d 100644
--- a/proofs/proof_bullet.mli
+++ b/proofs/proof_bullet.mli
@@ -14,7 +14,10 @@
 (*                                                        *)
 (**********************************************************)
 
-type t = Vernacexpr.bullet
+type t =
+    | Dash of int
+    | Star of int
+    | Plus of int
 
 (** A [behavior] is the data of a put function which
     is called when a bullet prefixes a tactic, a suggest function
@@ -42,12 +45,8 @@ val register_behavior : behavior -> unit
 val put : Proof.t -> t -> Proof.t
 val suggest : Proof.t -> Pp.t
 
-(**********************************************************)
-(*                                                        *)
-(*                     Default goal selector              *)
-(*                                                        *)
-(**********************************************************)
-
-val pr_goal_selector : Vernacexpr.goal_selector -> Pp.t
-val get_default_goal_selector : unit -> Vernacexpr.goal_selector
-
+(** Deprecated  *)
+val pr_goal_selector : Goal_select.t -> Pp.t
+[@@ocaml.deprecated "Please use [Goal_select.pr_goal_selector]"]
+val get_default_goal_selector : unit -> Goal_select.t
+[@@ocaml.deprecated "Please use [Goal_select.get_default_goal_selector]"]
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index fc7c437e6..842003bc8 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -83,6 +83,7 @@ type proof_ending =
   | Proved of Vernacexpr.opacity_flag *
               Misctypes.lident option *
               proof_object
+
 type proof_terminator = proof_ending -> unit
 type closed_proof = proof_object * proof_terminator
 
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 058e839b4..197f71ca9 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -5,6 +5,7 @@ Proof_type
 Logic
 Refine
 Proof
+Goal_select
 Proof_bullet
 Proof_global
 Redexpr