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, 12 insertions, 27 deletions

diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index a53c2395f0..f8449bcda1 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -498,16 +498,8 @@ let info_file f =
 (* The objects defined below should survive an arbitrary time,
    so we register them to coq save/undo mechanism. *)
 
-let my_bool_option name initval =
-  let flag = ref initval in
-  let access = fun () -> !flag in
-  let () = declare_bool_option
-    {optdepr = false;
-     optkey = ["Extraction"; name];
-     optread = access;
-     optwrite = (:=) flag }
-  in
-  access
+let my_bool_option name value =
+  declare_bool_option_and_ref ~depr:false ~key:["Extraction"; name] ~value
 
 (*s Extraction AccessOpaque *)
 
@@ -588,25 +580,18 @@ let () = declare_int_option
 
 (* This option controls whether "dummy lambda" are removed when a
    toplevel constant is defined. *)
-let conservative_types_ref = ref false
-let conservative_types () = !conservative_types_ref
-
-let () = declare_bool_option
-  {optdepr = false;
-   optkey = ["Extraction"; "Conservative"; "Types"];
-   optread = (fun () -> !conservative_types_ref);
-   optwrite = (fun b -> conservative_types_ref := b) }
-
+let conservative_types =
+  declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Extraction"; "Conservative"; "Types"]
+    ~value:false
 
 (* Allows to print a comment at the beginning of the output files *)
-let file_comment_ref = ref ""
-let file_comment () = !file_comment_ref
-
-let () = declare_string_option
-  {optdepr = false;
-   optkey = ["Extraction"; "File"; "Comment"];
-   optread = (fun () -> !file_comment_ref);
-   optwrite = (fun s -> file_comment_ref := s) }
+let file_comment =
+  declare_string_option_and_ref
+    ~depr:false
+    ~key:["Extraction"; "File"; "Comment"]
+    ~value:""
 
 (*s Extraction Lang *)