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, 19 insertions, 41 deletions

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 7d87fc0220..ec23355ce1 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -107,9 +107,9 @@ let with_full_print f a =
   and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in
   let old_rawprint = !Flags.raw_print in
   let old_printuniverses = !Constrextern.print_universes in
-  let old_printallowmatchdefaultclause = !Detyping.print_allow_match_default_clause in
+  let old_printallowmatchdefaultclause = Detyping.print_allow_match_default_clause () in
   Constrextern.print_universes := true;
-  Detyping.print_allow_match_default_clause := false;
+  Goptions.set_bool_option_value Detyping.print_allow_match_default_opt_name false;
   Flags.raw_print := true;
   Impargs.make_implicit_args false;
   Impargs.make_strict_implicit_args false;
@@ -122,7 +122,7 @@ let with_full_print f a =
     Impargs.make_contextual_implicit_args old_contextual_implicit_args;
     Flags.raw_print := old_rawprint;
     Constrextern.print_universes := old_printuniverses;
-    Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause;
+    Goptions.set_bool_option_value Detyping.print_allow_match_default_opt_name old_printallowmatchdefaultclause;
     Dumpglob.continue ();
     res
   with
@@ -132,7 +132,7 @@ let with_full_print f a =
         Impargs.make_contextual_implicit_args old_contextual_implicit_args;
         Flags.raw_print := old_rawprint;
         Constrextern.print_universes := old_printuniverses;
-        Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause;
+        Goptions.set_bool_option_value Detyping.print_allow_match_default_opt_name old_printallowmatchdefaultclause;
         Dumpglob.continue ();
         raise reraise
 
@@ -309,33 +309,18 @@ let add_Function is_general f =
 let pr_table env sigma = pr_table env sigma !from_function
 (*********************************)
 (* Debugging *)
-let functional_induction_rewrite_dependent_proofs = ref true
-let function_debug = ref false
-open Goptions
 
-let functional_induction_rewrite_dependent_proofs_sig =
-  {
-    optdepr = false;
-    optkey =  ["Functional";"Induction";"Rewrite";"Dependent"];
-    optread = (fun () -> !functional_induction_rewrite_dependent_proofs);
-    optwrite = (fun b -> functional_induction_rewrite_dependent_proofs := b)
-  }
-let () = declare_bool_option functional_induction_rewrite_dependent_proofs_sig
+let do_rewrite_dependent =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Functional";"Induction";"Rewrite";"Dependent"]
+    ~value:true
 
-let do_rewrite_dependent () = !functional_induction_rewrite_dependent_proofs = true
-
-let function_debug_sig =
-  {
-    optdepr = false;
-    optkey =  ["Function_debug"];
-    optread = (fun () -> !function_debug);
-    optwrite = (fun b -> function_debug := b)
-  }
-
-let () = declare_bool_option function_debug_sig
-
-
-let do_observe () = !function_debug
+let do_observe =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Function_debug"]
+    ~value:false
 
 let observe strm =
   if do_observe ()
@@ -405,18 +390,11 @@ let observe_tac ~header s tac =
 
 end
 
-let strict_tcc = ref false
-let is_strict_tcc () = !strict_tcc
-let strict_tcc_sig =
-  {
-    optdepr = false;
-    optkey =  ["Function_raw_tcc"];
-    optread = (fun () -> !strict_tcc);
-    optwrite = (fun b -> strict_tcc := b)
-  }
-
-let () = declare_bool_option strict_tcc_sig
-
+let is_strict_tcc =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Function_raw_tcc"]
+    ~value:false
 
 exception Building_graph of exn
 exception Defining_principle of exn