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

3 files changed, 14 insertions, 38 deletions

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 2e509921c1..3195f339b6 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1251,10 +1251,12 @@ let vernac_generalizable ~local =
   let local = Option.default true local in
   Implicit_quantifiers.declare_generalizable ~local
 
+let allow_sprop_opt_name = ["Allow";"StrictProp"]
+
 let () =
   declare_bool_option
     { optdepr  = false;
-      optkey   = ["Allow";"StrictProp"];
+      optkey   = allow_sprop_opt_name;
       optread  = (fun () -> Global.sprop_allowed());
       optwrite = Global.set_allow_sprop }
 
@@ -1435,27 +1437,6 @@ let () =
       optread  = CWarnings.get_flags;
       optwrite = CWarnings.set_flags }
 
-let () =
-  declare_string_option
-    { optdepr  = false;
-      optkey   = ["NativeCompute"; "Profile"; "Filename"];
-      optread  = Nativenorm.get_profile_filename;
-      optwrite = Nativenorm.set_profile_filename }
-
-let () =
-  declare_bool_option
-    { optdepr  = false;
-      optkey   = ["NativeCompute"; "Profiling"];
-      optread  = Nativenorm.get_profiling_enabled;
-      optwrite = Nativenorm.set_profiling_enabled }
-
-let () =
-  declare_bool_option
-    { optdepr  = false;
-      optkey   = ["NativeCompute"; "Timing"];
-      optread  = Nativenorm.get_timing_enabled;
-      optwrite = Nativenorm.set_timing_enabled }
-
 let _ =
   declare_bool_option
     { optdepr  = false;
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index f5cf9702cd..2ac8458ad5 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -24,3 +24,5 @@ val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr
 
 (** Miscellaneous stuff *)
 val command_focus : unit Proof.focus_kind
+
+val allow_sprop_opt_name : string list
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 15a19c06c2..eb299222dd 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -51,24 +51,17 @@ let interp_typed_vernac c ~stack =
 
 (* Default proof mode, to be set at the beginning of proofs for
    programs that cannot be statically classified. *)
-let default_proof_mode = ref (Pvernac.register_proof_mode "Noedit" Pvernac.Vernac_.noedit_mode)
-let get_default_proof_mode () = !default_proof_mode
+let proof_mode_opt_name = ["Default";"Proof";"Mode"]
 
-let get_default_proof_mode_opt () = Pvernac.proof_mode_to_string !default_proof_mode
-let set_default_proof_mode_opt name =
-  default_proof_mode :=
-    match Pvernac.lookup_proof_mode name with
+let get_default_proof_mode =
+  Goptions.declare_interpreted_string_option_and_ref
+    ~depr:false
+    ~key:proof_mode_opt_name
+    ~value:(Pvernac.register_proof_mode "Noedit" Pvernac.Vernac_.noedit_mode)
+    (fun name -> match Pvernac.lookup_proof_mode name with
     | Some pm -> pm
-    | None -> CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." name))
-
-let proof_mode_opt_name = ["Default";"Proof";"Mode"]
-let () =
-  Goptions.declare_string_option Goptions.{
-    optdepr = false;
-    optkey = proof_mode_opt_name;
-    optread = get_default_proof_mode_opt;
-    optwrite = set_default_proof_mode_opt;
-  }
+    | None -> CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." name)))
+    Pvernac.proof_mode_to_string
 
 (** A global default timeout, controlled by option "Set Default Timeout n".
     Use "Unset Default Timeout" to deactivate it (or set it to 0). *)