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, 5 insertions, 10 deletions

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)