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`.

2 files changed, 24 insertions, 38 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 () ++
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 63dae1417e..d464ec4c06 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -221,27 +221,17 @@ let build_env gamma=
                      mkApp(force node_count l_push,[|mkProp;p;e|]))
     gamma.env (mkApp (force node_count l_empty,[|mkProp|]))
 
-open Goptions
-
-let verbose = ref false
-
-let opt_verbose=
-  {optdepr=false;
-   optkey=["Rtauto";"Verbose"];
-   optread=(fun () -> !verbose);
-   optwrite=(fun b -> verbose:=b)}
-
-let () = declare_bool_option opt_verbose
-
-let check = ref false
-
-let opt_check=
-  {optdepr=false;
-   optkey=["Rtauto";"Check"];
-   optread=(fun () -> !check);
-   optwrite=(fun b -> check:=b)}
-
-let () = declare_bool_option opt_check
+let verbose =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Rtauto";"Verbose"]
+    ~value:false
+
+let check =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Rtauto";"Check"]
+    ~value:false
 
 open Pp
 
@@ -267,7 +257,7 @@ let rtauto_tac =
     let () =
       begin
         reset_info ();
-        if !verbose then
+        if verbose () then
           Feedback.msg_info (str "Starting proof-search ...");
       end in
     let search_start_time = System.get_time () in
@@ -276,7 +266,7 @@ let rtauto_tac =
       with Not_found ->
         user_err ~hdr:"rtauto" (Pp.str "rtauto couldn't find any proof") in
     let search_end_time = System.get_time () in
-    let () = if !verbose then
+    let () = if verbose () then
         begin
           Feedback.msg_info (str "Proof tree found in " ++
                              System.fmt_time_difference search_start_time search_end_time);
@@ -292,7 +282,7 @@ let rtauto_tac =
     let term=
       applistc main (List.rev_map (fun (id,_) -> mkVar id.binder_name) hyps) in
     let build_end_time=System.get_time () in
-    let () = if !verbose then
+    let () = if verbose () then
         begin
           Feedback.msg_info (str "Proof term built in " ++
                              System.fmt_time_difference build_start_time build_end_time ++
@@ -306,14 +296,14 @@ let rtauto_tac =
     let tac_start_time = System.get_time () in
     let term = EConstr.of_constr term in
     let result=
-      if !check then
+      if check () then
         Tactics.exact_check term
       else
         Tactics.exact_no_check term in
     let tac_end_time = System.get_time () in
     let () =
-      if !check then Feedback.msg_info (str "Proof term type-checking is on");
-      if !verbose then
+      if check () then Feedback.msg_info (str "Proof term type-checking is on");
+      if verbose () then
         Feedback.msg_info (str "Internal tactic executed in " ++
                            System.fmt_time_difference tac_start_time tac_end_time) in
     result