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, 7 insertions, 17 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 01f3537a7f..f7456ef35e 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -30,14 +30,6 @@ exception Elimconst
     their parameters in its stack.
 *)
 
-let () = Goptions.(declare_bool_option {
-  optdepr = false;
-  optkey = ["Cumulativity";"Weak";"Constraints"];
-  optread = (fun () -> not !UState.drop_weak_constraints);
-  optwrite = (fun a -> UState.drop_weak_constraints:=not a);
-})
-
-
 (** Support for reduction effects *)
 
 open Mod_subst
@@ -966,13 +958,11 @@ module CredNative = RedNative(CNativeEntries)
     contract_* in any case .
 *)
 
-let debug_RAKAM = ref (false)
-let () = Goptions.(declare_bool_option {
-  optdepr = false;
-  optkey = ["Debug";"RAKAM"];
-  optread = (fun () -> !debug_RAKAM);
-  optwrite = (fun a -> debug_RAKAM:=a);
-})
+let debug_RAKAM =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Debug";"RAKAM"]
+    ~value:false
 
 let equal_stacks sigma (x, l) (y, l') =
   let f_equal x y = eq_constr sigma x y in
@@ -983,7 +973,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
   let open Context.Named.Declaration in
   let open ReductionBehaviour in
   let rec whrec cst_l (x, stack) =
-    let () = if !debug_RAKAM then
+    let () = if debug_RAKAM () then
         let open Pp in
         let pr c = Termops.Internal.print_constr_env env sigma c in
         Feedback.msg_debug
@@ -994,7 +984,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
     in
     let c0 = EConstr.kind sigma x in
     let fold () =
-      let () = if !debug_RAKAM then
+      let () = if debug_RAKAM () then
           let open Pp in Feedback.msg_debug (str "<><><><><>") in
       ((EConstr.of_kind c0, stack),cst_l)
     in