Updated version 8.9.0 from 'upstream/8.9.0'

with Debian dir 81a4f85bc45e59aa1eadb4797f0eb0b8039efb63

1 files changed, 12 insertions, 56 deletions

diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml
index e22d382f..cc3e79f8 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,52 +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.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
-                                 })
-
+let pr_goal_selector = Goal_select.pr_goal_selector
+let get_default_goal_selector = Goal_select.get_default_goal_selector