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, 22 insertions, 21 deletions

diff --git a/engine/namegen.ml b/engine/namegen.ml
index 370f35f6ed..c4472050f8 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -219,22 +219,22 @@ let get_mangle_names =
     ~key:["Mangle";"Names"]
     ~value:false
 
-let mangle_names_prefix = ref (Id.of_string "_0")
-
-let set_prefix x = mangle_names_prefix := forget_subscript x
-
-let () = Goptions.(
-    declare_string_option
-      { optdepr  = false;
-        optkey   = ["Mangle";"Names";"Prefix"];
-        optread  = (fun () -> Id.to_string !mangle_names_prefix);
-        optwrite = begin fun x ->
-                   set_prefix
-                     (try Id.of_string x
-                      with CErrors.UserError _ -> CErrors.user_err Pp.(str ("Not a valid identifier: \"" ^ x ^ "\".")))
-                   end })
-
-let mangle_id id = if get_mangle_names () then !mangle_names_prefix else id
+let mangle_names_prefix =
+  Goptions.declare_interpreted_string_option_and_ref
+    ~depr:false
+    ~key:["Mangle";"Names";"Prefix"]
+    ~value:(Id.of_string "_0")
+    (fun x ->
+      (try
+         Id.of_string x
+       with
+       | CErrors.UserError _ ->
+          CErrors.user_err Pp.(str ("Not a valid identifier: \"" ^ x ^ "\"."))
+      ) |> forget_subscript
+    )
+    (fun x -> Id.to_string x)
+
+let mangle_id id = if get_mangle_names () then mangle_names_prefix () else id
 
 (* Looks for next "good" name by lifting subscript *)
 
diff --git a/engine/uState.ml b/engine/uState.ml
index d532129dc5..ff85f09efa 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -176,8 +176,11 @@ let instantiate_variable l b v =
 
 exception UniversesDiffer
 
-let drop_weak_constraints = ref false
-
+let drop_weak_constraints =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Cumulativity";"Weak";"Constraints"]
+    ~value:false
 
 let process_universe_constraints ctx cstrs =
   let open UnivSubst in
@@ -270,7 +273,7 @@ let process_universe_constraints ctx cstrs =
           | ULub (l, r) ->
               equalize_variables true (Universe.make l) l (Universe.make r) r local
           | UWeak (l, r) ->
-            if not !drop_weak_constraints then weak := UPairSet.add (l,r) !weak; local
+            if not (drop_weak_constraints ()) then weak := UPairSet.add (l,r) !weak; local
           | UEq (l, r) -> equalize_universes l r local
   in
   let local =
diff --git a/engine/uState.mli b/engine/uState.mli
index 3959373ead..cd1c9a174e 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -69,8 +69,6 @@ val univ_entry : poly:bool -> t -> Entries.universes_entry
 
 (** {5 Constraints handling} *)
 
-val drop_weak_constraints : bool ref
-
 val add_constraints : t -> Univ.Constraint.t -> t
 (**
   @raise UniversesDiffer when universes differ