[options] New helper for creation of boolean options plus reference.

This makes setting the option outside of the synchronized summary impossible.

2 files changed, 21 insertions, 36 deletions

diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index cbb77057bd..4926b8c3e1 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -337,32 +337,20 @@ let assumption_message = Declare.assumption_message
 let default_tactic = ref (Proofview.tclUNIT ())
 
 (* true = hide obligations *)
-let hide_obligations = ref false
-
-let set_hide_obligations = (:=) hide_obligations
-let get_hide_obligations () = !hide_obligations
-
-open Goptions
-let () =
-  declare_bool_option
-    { optdepr  = false;
-      optname  = "Hiding of Program obligations";
-      optkey   = ["Hide";"Obligations"];
-      optread  = get_hide_obligations;
-      optwrite = set_hide_obligations; }
-
-let shrink_obligations = ref true
-
-let set_shrink_obligations = (:=) shrink_obligations
-let get_shrink_obligations () = !shrink_obligations
-
-let () =
-  declare_bool_option
-    { optdepr  = true; (* remove in 8.8 *)
-      optname  = "Shrinking of Program obligations";
-      optkey   = ["Shrink";"Obligations"];
-      optread  = get_shrink_obligations;
-      optwrite = set_shrink_obligations; }
+let get_hide_obligations =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~name:"Hidding of Program obligations"
+    ~key:["Hide";"Obligations"]
+    ~value:false
+
+
+let get_shrink_obligations =
+  Goptions.declare_bool_option_and_ref
+    ~depr:true (* remove in 8.8 *)
+    ~name:"Shrinking of Program obligations"
+    ~key:["Shrink";"Obligations"]
+    ~value:true
 
 let evar_of_obligation o = make_evar (Global.named_context_val ()) (EConstr.of_constr o.obl_type)
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index fa1082473e..a157e01fc1 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -582,10 +582,15 @@ let should_treat_as_cumulative cum poly =
     else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.")
   | None -> poly && Flags.is_polymorphic_inductive_cumulativity ()
 
-let uniform_inductive_parameters = ref false
+let get_uniform_inductive_parameters =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~name:"Uniform inductive parameters"
+    ~key:["Uniform"; "Inductive"; "Parameters"]
+    ~value:false
 
 let should_treat_as_uniform () =
-  if !uniform_inductive_parameters
+  if get_uniform_inductive_parameters ()
   then ComInductive.UniformParameters
   else ComInductive.NonUniformParameters
 
@@ -1538,14 +1543,6 @@ let () =
       optwrite = Flags.make_polymorphic_inductive_cumulativity }
 
 let () =
-  declare_bool_option
-    { optdepr  = false;
-      optname  = "Uniform inductive parameters";
-      optkey   = ["Uniform"; "Inductive"; "Parameters"];
-      optread  = (fun () -> !uniform_inductive_parameters);
-      optwrite = (fun b -> uniform_inductive_parameters := b) }
-
-let () =
   declare_int_option
     { optdepr  = false;
       optname  = "the level of inlining during functor application";