Clean and fix definitions of options.

- Provide new helper functions in `Goptions` on the model of
  `declare_bool_option_and_ref`;

- Use these helper functions in many parts of the code base
  (encapsulates the corresponding references);

- Move almost all options from `declare_string_option` to
  `declare_stringopt_option` (only "Warnings" continue to use the
  former).  This means that these options now support `Unset` to get
  back to the default setting.  Note that there is a naming
  misalignment since `declare_int_option` is similar to
  `declare_stringopt_option` and supports `Unset`.  When "Warning" is
  eventually migrated to support `Unset` as well, we can remove
  `declare_string_option` and rename `declare_stringopt_option` to
  `declare_string_option`.

- For some vernac options and flags that have an equivalent
  command-line option or flag, implement it like the standard `-set`
  and `-unset`.

2 files changed, 21 insertions, 35 deletions

diff --git a/proofs/goal_select.ml b/proofs/goal_select.ml
index 29e19778e4..e847535aaf 100644
--- a/proofs/goal_select.ml
+++ b/proofs/goal_select.ml
@@ -22,11 +22,6 @@ type t =
   | 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)
@@ -53,15 +48,12 @@ let parse_goal_selector = function
         with Failure _ -> CErrors.user_err Pp.(str err_msg)
       end
 
-let () = let open Goptions in
-  declare_string_option
-    { optdepr = false;
-      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
-    }
+(* Default goal selector: selector chosen when a tactic is applied
+   without an explicit selector. *)
+let get_default_goal_selector =
+  Goptions.declare_interpreted_string_option_and_ref
+    ~depr:false
+    ~key:["Default";"Goal";"Selector"]
+    ~value:(SelectNth 1)
+    parse_goal_selector
+    (fun v -> Pp.string_of_ppcmds @@ pr_goal_selector v)
diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml
index f1f7361317..f619bc86a1 100644
--- a/proofs/proof_bullet.ml
+++ b/proofs/proof_bullet.ml
@@ -174,28 +174,22 @@ module Strict = struct
 end
 
 (* Current bullet behavior, controlled by the option *)
-let current_behavior = ref Strict.strict
-
-let () =
-  Goptions.(declare_string_option {
-    optdepr = false;
-    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 current_behavior =
+  Goptions.declare_interpreted_string_option_and_ref
+    ~depr:false
+    ~key:["Bullet";"Behavior"]
+    ~value:Strict.strict
+    (fun n ->
+      try Hashtbl.find behaviors n
+      with Not_found ->
+        CErrors.user_err Pp.(str ("Unknown bullet behavior: \"" ^ n ^ "\".")))
+    (fun v -> v.name)
 
 let put p b =
-  (!current_behavior).put p b
+  (current_behavior ()).put p b
 
 let suggest p =
-  (!current_behavior).suggest p
+  (current_behavior ()).suggest p
 
 (* Better printing for bullet exceptions *)
 exception SuggestNoSuchGoals of int * Proof.t