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

1 files changed, 15 insertions, 20 deletions

diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index f989dae4c9..c1ca40329a 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -28,16 +28,22 @@ exception Find_at of int
 
 (* timing *)
 
-let timing_enabled = ref false
+let get_timing_enabled =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["NativeCompute"; "Timing"]
+    ~value:false
 
 (* profiling *)
 
-let profiling_enabled = ref false
+let get_profiling_enabled =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["NativeCompute"; "Profiling"]
+    ~value:false
 
 (* for supported platforms, filename for profiler results *)
 
-let profile_filename = ref "native_compute_profile.data"
-
 let profiler_platform () =
   match [@warning "-8"] Sys.os_type with
   | "Unix" ->
@@ -48,10 +54,11 @@ let profiler_platform () =
   | "Win32" -> "Windows (Win32)"
   | "Cygwin" -> "Windows (Cygwin)"
 
-let get_profile_filename () = !profile_filename
-
-let set_profile_filename fn =
-  profile_filename := fn
+let get_profile_filename =
+  Goptions.declare_string_option_and_ref
+    ~depr:false
+    ~key:["NativeCompute"; "Profile"; "Filename"]
+    ~value:"native_compute_profile.data"
 
 (* find unused profile filename *)
 let get_available_profile_filename () =
@@ -77,18 +84,6 @@ let get_available_profile_filename () =
     let _ = Feedback.msg_info (Pp.str msg) in
     assert false
 
-let get_profiling_enabled () =
-  !profiling_enabled
-
-let set_profiling_enabled b =
-  profiling_enabled := b
-
-let get_timing_enabled () =
-  !timing_enabled
-
-let set_timing_enabled b =
-  timing_enabled := b
-
 let invert_tag cst tag reloc_tbl =
   try
     for j = 0 to Array.length reloc_tbl - 1 do