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, 6 insertions, 11 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 74043d6bc8..6f5c910297 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -25,19 +25,14 @@ open Util
 
 let init_size=5
 
-let cc_verbose=ref false
+let cc_verbose=
+  declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Congruence";"Verbose"]
+    ~value:false
 
 let debug x =
-  if !cc_verbose then Feedback.msg_debug (x ())
-
-let () =
-  let gdopt=
-    { optdepr=false;
-      optkey=["Congruence";"Verbose"];
-      optread=(fun ()-> !cc_verbose);
-      optwrite=(fun b -> cc_verbose := b)}
-  in
-    declare_bool_option gdopt
+  if cc_verbose () then Feedback.msg_debug (x ())
 
 (* Signature table *)