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

diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 537c37810e..1371c671a2 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -45,15 +45,11 @@ let reset_info () =
      s_info.branch_successes <- 0;
      s_info.nd_branching     <- 0
 
-let pruning = ref true
-
-let opt_pruning=
-  {optdepr=false;
-   optkey=["Rtauto";"Pruning"];
-   optread=(fun () -> !pruning);
-   optwrite=(fun b -> pruning:=b)}
-
-let () = declare_bool_option opt_pruning
+let pruning =
+  declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Rtauto";"Pruning"]
+    ~value:true
 
 type form=
     Atom of int
@@ -182,7 +178,7 @@ let rec fill stack proof =
       [] -> Complete proof.dep_it
     | slice::super ->
         if
-          !pruning &&
+          pruning () &&
           List.is_empty slice.proofs_done &&
           not (slice.changes_goal && proof.dep_goal) &&
           not (Int.Set.exists
@@ -529,7 +525,7 @@ let pp =
 
 let pp_info () =
   let count_info =
-    if !pruning then
+    if pruning () then
         str "Proof steps : " ++
         int s_info.created_steps ++ str " created / " ++
         int s_info.pruned_steps ++ str " pruned" ++ fnl () ++