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, 3 insertions, 15 deletions

diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg
index 49e4c91182..6ddc6ba21e 100644
--- a/plugins/firstorder/g_ground.mlg
+++ b/plugins/firstorder/g_ground.mlg
@@ -31,20 +31,8 @@ DECLARE PLUGIN "ground_plugin"
 
 {
 
-let ground_depth=ref 3
-
-let ()=
-  let gdopt=
-    { optdepr=false;
-      optkey=["Firstorder";"Depth"];
-      optread=(fun ()->Some !ground_depth);
-      optwrite=
-   (function
-        None->ground_depth:=3
-      |	Some i->ground_depth:=(max i 0))}
-  in
-    declare_int_option gdopt
-
+let ground_depth =
+  declare_nat_option_and_ref ~depr:false ~key:["Firstorder";"Depth"] ~value:3
 
 let default_intuition_tac =
   let tac _ _ = Auto.h_auto None [] (Some []) in
@@ -85,7 +73,7 @@ let gen_ground_tac flag taco ids bases =
           | None-> snd (default_solver ()) in
       let startseq k =
         Proofview.Goal.enter begin fun gl ->
-        let seq=empty_seq !ground_depth in
+        let seq=empty_seq (ground_depth ()) in
         let seq, sigma = extend_with_ref_list (pf_env gl) (project gl) ids seq in
         let seq, sigma = extend_with_auto_hints (pf_env gl) sigma bases seq in
         tclTHEN (Proofview.Unsafe.tclEVARS sigma) (k seq)