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

10 files changed, 104 insertions, 221 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 *)
 
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 *)
 
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)
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 7d87fc0220..ec23355ce1 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -107,9 +107,9 @@ let with_full_print f a =
   and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in
   let old_rawprint = !Flags.raw_print in
   let old_printuniverses = !Constrextern.print_universes in
-  let old_printallowmatchdefaultclause = !Detyping.print_allow_match_default_clause in
+  let old_printallowmatchdefaultclause = Detyping.print_allow_match_default_clause () in
   Constrextern.print_universes := true;
-  Detyping.print_allow_match_default_clause := false;
+  Goptions.set_bool_option_value Detyping.print_allow_match_default_opt_name false;
   Flags.raw_print := true;
   Impargs.make_implicit_args false;
   Impargs.make_strict_implicit_args false;
@@ -122,7 +122,7 @@ let with_full_print f a =
     Impargs.make_contextual_implicit_args old_contextual_implicit_args;
     Flags.raw_print := old_rawprint;
     Constrextern.print_universes := old_printuniverses;
-    Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause;
+    Goptions.set_bool_option_value Detyping.print_allow_match_default_opt_name old_printallowmatchdefaultclause;
     Dumpglob.continue ();
     res
   with
@@ -132,7 +132,7 @@ let with_full_print f a =
         Impargs.make_contextual_implicit_args old_contextual_implicit_args;
         Flags.raw_print := old_rawprint;
         Constrextern.print_universes := old_printuniverses;
-        Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause;
+        Goptions.set_bool_option_value Detyping.print_allow_match_default_opt_name old_printallowmatchdefaultclause;
         Dumpglob.continue ();
         raise reraise
 
@@ -309,33 +309,18 @@ let add_Function is_general f =
 let pr_table env sigma = pr_table env sigma !from_function
 (*********************************)
 (* Debugging *)
-let functional_induction_rewrite_dependent_proofs = ref true
-let function_debug = ref false
-open Goptions
 
-let functional_induction_rewrite_dependent_proofs_sig =
-  {
-    optdepr = false;
-    optkey =  ["Functional";"Induction";"Rewrite";"Dependent"];
-    optread = (fun () -> !functional_induction_rewrite_dependent_proofs);
-    optwrite = (fun b -> functional_induction_rewrite_dependent_proofs := b)
-  }
-let () = declare_bool_option functional_induction_rewrite_dependent_proofs_sig
+let do_rewrite_dependent =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Functional";"Induction";"Rewrite";"Dependent"]
+    ~value:true
 
-let do_rewrite_dependent () = !functional_induction_rewrite_dependent_proofs = true
-
-let function_debug_sig =
-  {
-    optdepr = false;
-    optkey =  ["Function_debug"];
-    optread = (fun () -> !function_debug);
-    optwrite = (fun b -> function_debug := b)
-  }
-
-let () = declare_bool_option function_debug_sig
-
-
-let do_observe () = !function_debug
+let do_observe =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Function_debug"]
+    ~value:false
 
 let observe strm =
   if do_observe ()
@@ -405,18 +390,11 @@ let observe_tac ~header s tac =
 
 end
 
-let strict_tcc = ref false
-let is_strict_tcc () = !strict_tcc
-let strict_tcc_sig =
-  {
-    optdepr = false;
-    optkey =  ["Function_raw_tcc"];
-    optread = (fun () -> !strict_tcc);
-    optwrite = (fun b -> strict_tcc := b)
-  }
-
-let () = declare_bool_option strict_tcc_sig
-
+let is_strict_tcc =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Function_raw_tcc"]
+    ~value:false
 
 exception Building_graph of exn
 exception Defining_principle of exn
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 50c3ed1248..2bd4211c90 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -359,21 +359,15 @@ open Vernacextend
 open Goptions
 open Libnames
 
-let print_info_trace = ref None
-
-let () = declare_int_option {
-  optdepr = false;
-  optkey = ["Info" ; "Level"];
-  optread = (fun () -> !print_info_trace);
-  optwrite = fun n -> print_info_trace := n;
-}
+let print_info_trace =
+  declare_intopt_option_and_ref ~depr:false ~key:["Info" ; "Level"]
 
 let vernac_solve ~pstate n info tcom b =
   let open Goal_select in
   let pstate, status = Proof_global.map_fold_proof_endline (fun etac p ->
       let with_end_tac = if b then Some etac else None in
       let global = match n with SelectAll | SelectList _ -> true | _ -> false in
-      let info = Option.append info !print_info_trace in
+      let info = Option.append info (print_info_trace ()) in
       let (p,status) =
         Pfedit.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p
       in
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 1958fff4cc..9eeba614c7 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -27,7 +27,13 @@ open NumCompat
 open Q.Notations
 open Mutils
 
-let use_simplex = ref true
+let use_simplex =
+  Goptions.declare_bool_option_and_ref ~depr:false ~key:["Simplex"] ~value:true
+
+(* If set to some [file], arithmetic goals are dumped in [file].v *)
+
+let dump_file =
+  Goptions.declare_stringopt_option_and_ref ~depr:false ~key:["Dump"; "Arith"]
 
 type ('prf, 'model) res = Prf of 'prf | Model of 'model | Unknown
 type zres = (Mc.zArithProof, int * Mc.z list) res
@@ -203,19 +209,19 @@ let fourier_linear_prover l =
   | Inl _ -> None
 
 let direct_linear_prover l =
-  if !use_simplex then Simplex.find_unsat_certificate l
+  if use_simplex () then Simplex.find_unsat_certificate l
   else fourier_linear_prover l
 
 let find_point l =
   let open Util in
-  if !use_simplex then Simplex.find_point l
+  if use_simplex () then Simplex.find_point l
   else
     match Mfourier.Fourier.find_point l with
     | Inr _ -> None
     | Inl cert -> Some cert
 
 let optimise v l =
-  if !use_simplex then Simplex.optimise v l else Mfourier.Fourier.optimise v l
+  if use_simplex () then Simplex.optimise v l else Mfourier.Fourier.optimise v l
 
 let dual_raw_certificate l =
   if debug then begin
@@ -981,13 +987,11 @@ let xlia_simplex env red sys =
   with FoundProof prf -> compile_prf sys (Step (0, prf, Done))
 
 let xlia env0 en red sys =
-  if !use_simplex then xlia_simplex env0 red sys else xlia en red sys
-
-let dump_file = ref None
+  if use_simplex () then xlia_simplex env0 red sys else xlia en red sys
 
 let gen_bench (tac, prover) can_enum prfdepth sys =
   let res = prover can_enum prfdepth sys in
-  ( match !dump_file with
+  ( match dump_file () with
   | None -> ()
   | Some file ->
     let o = open_out (Filename.temp_file ~temp_dir:(Sys.getcwd ()) file ".v") in
diff --git a/plugins/micromega/certificate.mli b/plugins/micromega/certificate.mli
index cabd36ebb7..5b215549b0 100644
--- a/plugins/micromega/certificate.mli
+++ b/plugins/micromega/certificate.mli
@@ -12,16 +12,12 @@ module Mc = Micromega
 
 (** [use_simplex] is bound to the Coq option Simplex.
     If set, use the Simplex method, otherwise use Fourier *)
-val use_simplex : bool ref
+val use_simplex : unit -> bool
 
 type ('prf, 'model) res = Prf of 'prf | Model of 'model | Unknown
 type zres = (Mc.zArithProof, int * Mc.z list) res
 type qres = (Mc.q Mc.psatz, int * Mc.q list) res
 
-(** [dump_file] is bound to the Coq option Dump Arith.
-    If set to some [file], arithmetic goals are dumped in filexxx.v *)
-val dump_file : string option ref
-
 (** [q_cert_of_pos prf] converts a Sos proof into a rational Coq proof *)
 val q_cert_of_pos : Sos_types.positivstellensatz -> Mc.q Mc.psatz
 
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 43f6f5a35e..7e4c4ce5c6 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -37,74 +37,31 @@ let debug = false
 let max_depth = max_int
 
 (* Search limit for provers over Q R *)
-let lra_proof_depth = ref max_depth
+let lra_proof_depth =
+  declare_int_option_and_ref ~depr:false ~key:["Lra"; "Depth"] ~value:max_depth
 
 (* Search limit for provers over Z *)
-let lia_enum = ref true
-let lia_proof_depth = ref max_depth
-let get_lia_option () = (!Certificate.use_simplex, !lia_enum, !lia_proof_depth)
-let get_lra_option () = !lra_proof_depth
+let lia_enum =
+  declare_bool_option_and_ref ~depr:false ~key:["Lia"; "Enum"] ~value:true
+
+let lia_proof_depth =
+  declare_int_option_and_ref ~depr:false ~key:["Lia"; "Depth"] ~value:max_depth
+
+let get_lia_option () =
+  (Certificate.use_simplex (), lia_enum (), lia_proof_depth ())
 
 (* Enable/disable caches *)
 
-let use_lia_cache = ref true
-let use_nia_cache = ref true
-let use_nra_cache = ref true
-let use_csdp_cache = ref true
-
-let () =
-  let int_opt l vref =
-    { optdepr = false
-    ; optkey = l
-    ; optread = (fun () -> Some !vref)
-    ; optwrite =
-        (fun x -> vref := match x with None -> max_depth | Some v -> v) }
-  in
-  let lia_enum_opt =
-    { optdepr = false
-    ; optkey = ["Lia"; "Enum"]
-    ; optread = (fun () -> !lia_enum)
-    ; optwrite = (fun x -> lia_enum := x) }
-  in
-  let solver_opt =
-    { optdepr = false
-    ; optkey = ["Simplex"]
-    ; optread = (fun () -> !Certificate.use_simplex)
-    ; optwrite = (fun x -> Certificate.use_simplex := x) }
-  in
-  let dump_file_opt =
-    { optdepr = false
-    ; optkey = ["Dump"; "Arith"]
-    ; optread = (fun () -> !Certificate.dump_file)
-    ; optwrite = (fun x -> Certificate.dump_file := x) }
-  in
-  let lia_cache_opt =
-    { optdepr = false
-    ; optkey = ["Lia"; "Cache"]
-    ; optread = (fun () -> !use_lia_cache)
-    ; optwrite = (fun x -> use_lia_cache := x) }
-  in
-  let nia_cache_opt =
-    { optdepr = false
-    ; optkey = ["Nia"; "Cache"]
-    ; optread = (fun () -> !use_nia_cache)
-    ; optwrite = (fun x -> use_nia_cache := x) }
-  in
-  let nra_cache_opt =
-    { optdepr = false
-    ; optkey = ["Nra"; "Cache"]
-    ; optread = (fun () -> !use_nra_cache)
-    ; optwrite = (fun x -> use_nra_cache := x) }
-  in
-  let () = declare_bool_option solver_opt in
-  let () = declare_bool_option lia_cache_opt in
-  let () = declare_bool_option nia_cache_opt in
-  let () = declare_bool_option nra_cache_opt in
-  let () = declare_stringopt_option dump_file_opt in
-  let () = declare_int_option (int_opt ["Lra"; "Depth"] lra_proof_depth) in
-  let () = declare_int_option (int_opt ["Lia"; "Depth"] lia_proof_depth) in
-  let () = declare_bool_option lia_enum_opt in
-  ()
+let use_lia_cache =
+  declare_bool_option_and_ref ~depr:false ~key:["Lia"; "Cache"] ~value:true
+
+let use_nia_cache =
+  declare_bool_option_and_ref ~depr:false ~key:["Nia"; "Cache"] ~value:true
+
+let use_nra_cache =
+  declare_bool_option_and_ref ~depr:false ~key:["Nra"; "Cache"] ~value:true
+
+let use_csdp_cache () = true
 
 (**
   * Initialize a tag type to the Tag module declaration (see Mutils).
@@ -2101,7 +2058,7 @@ struct
 
   let memo_opt use_cache cache_file f =
     let memof = memo cache_file f in
-    fun x -> if !use_cache then memof x else f x
+    fun x -> if use_cache () then memof x else f x
 end
 
 module CacheCsdp = MakeCache (struct
@@ -2281,7 +2238,7 @@ let memo_nra =
 
 let linear_prover_Q =
   { name = "linear prover"
-  ; get_option = get_lra_option
+  ; get_option = lra_proof_depth
   ; prover =
       (fun (o, l) ->
         lift_pexpr_prover (Certificate.linear_prover_with_cert o) l)
@@ -2292,7 +2249,7 @@ let linear_prover_Q =
 
 let linear_prover_R =
   { name = "linear prover"
-  ; get_option = get_lra_option
+  ; get_option = lra_proof_depth
   ; prover =
       (fun (o, l) ->
         lift_pexpr_prover (Certificate.linear_prover_with_cert o) l)
@@ -2303,7 +2260,7 @@ let linear_prover_R =
 
 let nlinear_prover_R =
   { name = "nra"
-  ; get_option = get_lra_option
+  ; get_option = lra_proof_depth
   ; prover = memo_nra
   ; hyps = hyps_of_cone
   ; compact = compact_cone
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