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

6 files changed, 75 insertions, 115 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 92d56d2904..57eab7ddf8 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -38,33 +38,48 @@ let typeclasses_db = "typeclass_instances"
 (** Options handling *)
 
 let typeclasses_debug = ref 0
-let typeclasses_depth = ref None
+
+let typeclasses_depth_opt_name = ["Typeclasses";"Depth"]
+let get_typeclasses_depth =
+  Goptions.declare_intopt_option_and_ref
+    ~depr:false
+    ~key:typeclasses_depth_opt_name
+
+let set_typeclasses_depth =
+  Goptions.set_int_option_value typeclasses_depth_opt_name
 
 (** When this flag is enabled, the resolution of type classes tries to avoid
     useless introductions. This is no longer useful since we have eta, but is
     here for compatibility purposes. Another compatibility issues is that the
     cost (in terms of search depth) can differ. *)
-let typeclasses_limit_intros = ref true
-let set_typeclasses_limit_intros d = (:=) typeclasses_limit_intros d
-let get_typeclasses_limit_intros () = !typeclasses_limit_intros
-
-let typeclasses_dependency_order = ref false
-let set_typeclasses_dependency_order d = (:=) typeclasses_dependency_order d
-let get_typeclasses_dependency_order () = !typeclasses_dependency_order
-
-let typeclasses_iterative_deepening = ref false
-let set_typeclasses_iterative_deepening d = (:=) typeclasses_iterative_deepening d
-let get_typeclasses_iterative_deepening () = !typeclasses_iterative_deepening
+let get_typeclasses_limit_intros =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Typeclasses";"Limit";"Intros"]
+    ~value:true
+
+let get_typeclasses_dependency_order =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Typeclasses";"Dependency";"Order"]
+    ~value:false
+
+let iterative_deepening_opt_name = ["Typeclasses";"Iterative";"Deepening"]
+let get_typeclasses_iterative_deepening =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:iterative_deepening_opt_name
+    ~value:false
 
 (** [typeclasses_filtered_unif] governs the unification algorithm used by type
     classes. If enabled, a new algorithm based on pattern filtering and refine
     will be used. When disabled, the previous algorithm based on apply will be
     used. *)
-let typeclasses_filtered_unification = ref false
-let set_typeclasses_filtered_unification d =
-  (:=) typeclasses_filtered_unification d
-let get_typeclasses_filtered_unification () =
-  !typeclasses_filtered_unification
+let get_typeclasses_filtered_unification =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Typeclasses";"Filtered";"Unification"]
+    ~value:false
 
 let set_typeclasses_debug d = (:=) typeclasses_debug (if d then 1 else 0)
 let get_typeclasses_debug () = if !typeclasses_debug > 0 then true else false
@@ -75,40 +90,8 @@ let set_typeclasses_verbose =
 let get_typeclasses_verbose () =
   if !typeclasses_debug = 0 then None else Some !typeclasses_debug
 
-let set_typeclasses_depth d = (:=) typeclasses_depth d
-let get_typeclasses_depth () = !typeclasses_depth
-
-open Goptions
-
-let () =
-  declare_bool_option
-    { optdepr  = false;
-      optkey   = ["Typeclasses";"Limit";"Intros"];
-      optread  = get_typeclasses_limit_intros;
-      optwrite = set_typeclasses_limit_intros; }
-
-let () =
-  declare_bool_option
-    { optdepr  = false;
-      optkey   = ["Typeclasses";"Dependency";"Order"];
-      optread  = get_typeclasses_dependency_order;
-      optwrite = set_typeclasses_dependency_order; }
-
-let () =
-  declare_bool_option
-    { optdepr  = false;
-      optkey   = ["Typeclasses";"Iterative";"Deepening"];
-      optread  = get_typeclasses_iterative_deepening;
-      optwrite = set_typeclasses_iterative_deepening; }
-
-let () =
-  declare_bool_option
-    { optdepr  = false;
-      optkey   = ["Typeclasses";"Filtered";"Unification"];
-      optread  = get_typeclasses_filtered_unification;
-      optwrite = set_typeclasses_filtered_unification; }
-
 let () =
+  let open Goptions in
   declare_bool_option
     { optdepr  = false;
       optkey   = ["Typeclasses";"Debug"];
@@ -116,24 +99,18 @@ let () =
       optwrite = set_typeclasses_debug; }
 
 let _ =
+  let open Goptions in
   declare_int_option
     { optdepr  = false;
       optkey   = ["Typeclasses";"Debug";"Verbosity"];
       optread  = get_typeclasses_verbose;
       optwrite = set_typeclasses_verbose; }
 
-let () =
-  declare_int_option
-    { optdepr  = false;
-      optkey   = ["Typeclasses";"Depth"];
-      optread  = get_typeclasses_depth;
-      optwrite = set_typeclasses_depth; }
-
 type search_strategy = Dfs | Bfs
 
 let set_typeclasses_strategy = function
-  | Dfs -> set_typeclasses_iterative_deepening false
-  | Bfs -> set_typeclasses_iterative_deepening true
+  | Dfs -> Goptions.set_bool_option_value iterative_deepening_opt_name false
+  | Bfs -> Goptions.set_bool_option_value iterative_deepening_opt_name true
 
 let pr_ev evs ev =
   Printer.pr_econstr_env (Goal.V82.env evs ev) evs (Goal.V82.concl evs ev)
@@ -977,7 +954,7 @@ module Search = struct
     | None -> None (* This happens only because there's no evar having p *)
     | Some (goals, nongoals) ->
        let goalsl =
-         if !typeclasses_dependency_order then
+         if get_typeclasses_dependency_order () then
            top_sort evm goals
          else Evar.Set.elements goals
        in
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index e26338436d..b97b90d777 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -19,10 +19,8 @@ val catchable : exn -> bool
 [@@ocaml.deprecated "Use instead CErrors.noncritical, or the exact name of the exception that matters in the corresponding case."]
 
 val set_typeclasses_debug : bool -> unit
-val get_typeclasses_debug : unit -> bool
 
 val set_typeclasses_depth : int option -> unit
-val get_typeclasses_depth : unit -> int option
 
 type search_strategy = Dfs | Bfs
 
diff --git a/tactics/hints.ml b/tactics/hints.ml
index a907b9e783..f8a46fcb1d 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -188,27 +188,26 @@ type hints_expr =
   | HintsConstructors of qualid list
   | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
 
-type import_level = [ `LAX | `WARN | `STRICT ]
-
-let warn_hint : import_level ref = ref `LAX
-let read_warn_hint () = match !warn_hint with
-| `LAX -> "Lax"
-| `WARN -> "Warn"
-| `STRICT -> "Strict"
-
-let write_warn_hint = function
-| "Lax" -> warn_hint := `LAX
-| "Warn" -> warn_hint := `WARN
-| "Strict" -> warn_hint := `STRICT
-| _ -> user_err Pp.(str "Only the following flags are accepted: Lax, Warn, Strict.")
-
-let () =
-  Goptions.(declare_string_option
-    { optdepr  = false;
-      optkey   = ["Loose"; "Hint"; "Behavior"];
-      optread  = read_warn_hint;
-      optwrite = write_warn_hint;
-    })
+type import_level = HintLax | HintWarn | HintStrict
+
+let warn_hint_to_string = function
+| HintLax -> "Lax"
+| HintWarn -> "Warn"
+| HintStrict -> "Strict"
+
+let string_to_warn_hint = function
+| "Lax" -> HintLax
+| "Warn" -> HintWarn
+| "Strict" -> HintStrict
+| _ -> user_err Pp.(str "Only the following values are accepted: Lax, Warn, Strict.")
+
+let warn_hint =
+  Goptions.declare_interpreted_string_option_and_ref
+    ~depr:false
+    ~key:["Loose"; "Hint"; "Behavior"]
+    ~value:HintLax
+    string_to_warn_hint
+    warn_hint_to_string
 
 let fresh_key =
   let id = Summary.ref ~name:"HINT-COUNTER" 0 in
@@ -1690,12 +1689,12 @@ let wrap_hint_warning_fun env sigma t =
   in
   (ans, set_extra_data store sigma)
 
-let run_hint tac k = match !warn_hint with
-| `LAX -> k tac.obj
-| `WARN ->
+let run_hint tac k = match warn_hint () with
+| HintLax -> k tac.obj
+| HintWarn ->
   if is_imported tac then k tac.obj
   else Proofview.tclTHEN (log_hint tac) (k tac.obj)
-| `STRICT ->
+| HintStrict ->
   if is_imported tac then k tac.obj
   else Proofview.tclZERO (UserError (None, (str "Tactic failure.")))
 
diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml
index 22d0ce5328..c139594f13 100644
--- a/tactics/pfedit.ml
+++ b/tactics/pfedit.ml
@@ -14,15 +14,11 @@ open Names
 open Environ
 open Evd
 
-let use_unification_heuristics_ref = ref true
-let () = Goptions.(declare_bool_option {
-  optdepr = false;
-  optkey = ["Solve";"Unification";"Constraints"];
-  optread = (fun () -> !use_unification_heuristics_ref);
-  optwrite = (fun a -> use_unification_heuristics_ref:=a);
-})
-
-let use_unification_heuristics () = !use_unification_heuristics_ref
+let use_unification_heuristics =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Solve";"Unification";"Constraints"]
+    ~value:true
 
 exception NoSuchGoal
 let () = CErrors.register_handler begin function
diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml
index d7dcc13e79..68de9c7a00 100644
--- a/tactics/proof_global.ml
+++ b/tactics/proof_global.ml
@@ -130,15 +130,10 @@ let get_open_goals ps =
 type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t
 
 let private_poly_univs =
-  let b = ref true in
-  let _ = Goptions.(declare_bool_option {
-      optdepr = false;
-      optkey = ["Private";"Polymorphic";"Universes"];
-      optread = (fun () -> !b);
-      optwrite = ((:=) b);
-    })
-  in
-  fun () -> !b
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Private";"Polymorphic";"Universes"]
+    ~value:true
 
 (* XXX: This is still separate from close_proof below due to drop_pt in the STM *)
 let return_proof { proof } =
diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml
index db09a2e69e..f681e4e99e 100644
--- a/tactics/redexpr.ml
+++ b/tactics/redexpr.ml
@@ -53,13 +53,8 @@ let whd_cbn flags env sigma t =
 let strong_cbn flags =
   strong_with_flags whd_cbn flags
 
-let simplIsCbn = ref (false)
-let () = Goptions.(declare_bool_option {
-  optdepr = false;
-  optkey = ["SimplIsCbn"];
-  optread = (fun () -> !simplIsCbn);
-  optwrite = (fun a -> simplIsCbn:=a);
-})
+let simplIsCbn =
+  Goptions.declare_bool_option_and_ref ~depr:false ~key:["SimplIsCbn"] ~value:false
 
 let set_strategy_one ref l  =
   let k =
@@ -228,10 +223,10 @@ let reduction_of_red_expr env =
       else (e_red red_product,DEFAULTcast)
   | Hnf -> (e_red hnf_constr,DEFAULTcast)
   | Simpl (f,o) ->
-     let whd_am = if !simplIsCbn then whd_cbn (make_flag f) else whd_simpl in
-     let am = if !simplIsCbn then strong_cbn (make_flag f) else simpl in
+     let whd_am = if simplIsCbn () then whd_cbn (make_flag f) else whd_simpl in
+     let am = if simplIsCbn () then strong_cbn (make_flag f) else simpl in
      let () =
-       if not (!simplIsCbn || List.is_empty f.rConst) then
+       if not (simplIsCbn () || List.is_empty f.rConst) then
          warn_simpl_unfolding_modifiers () in
      (contextualize (if head_style then whd_am else am) am o,DEFAULTcast)
   | Cbv f -> (e_red (cbv_norm_flags (make_flag f)),DEFAULTcast)