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

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

19 files changed, 118 insertions, 171 deletions

diff --git a/engine/namegen.ml b/engine/namegen.ml
index 0f346edd3e..a67ff6965b 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -208,23 +208,16 @@ let it_mkLambda_or_LetIn_name env sigma b hyps =
 (* Introduce a mode where auto-generated names are mangled
    to test dependence of scripts on auto-generated names *)
 
-let mangle_names = ref false
-
-let () = Goptions.(
-    declare_bool_option
-      { optdepr  = false;
-        optname  = "mangle auto-generated names";
-        optkey   = ["Mangle";"Names"];
-        optread  = (fun () -> !mangle_names);
-        optwrite = (:=) mangle_names; })
+let get_mangle_names =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~name:"mangle auto-generated names"
+    ~key:["Mangle";"Names"]
+    ~value:false
 
 let mangle_names_prefix = ref (Id.of_string "_0")
-let set_prefix x = mangle_names_prefix := forget_subscript x
 
-let set_mangle_names_mode x = begin
-    set_prefix x;
-    mangle_names := true
-  end
+let set_prefix x = mangle_names_prefix := forget_subscript x
 
 let () = Goptions.(
     declare_string_option
@@ -238,7 +231,7 @@ let () = Goptions.(
                       with CErrors.UserError _ -> CErrors.user_err Pp.(str ("Not a valid identifier: \"" ^ x ^ "\".")))
                    end })
 
-let mangle_id id = if !mangle_names then !mangle_names_prefix else id
+let mangle_id id = if get_mangle_names () then !mangle_names_prefix else id
 
 (* Looks for next "good" name by lifting subscript *)
 
diff --git a/engine/namegen.mli b/engine/namegen.mli
index a53c3a0d1f..3722cbed24 100644
--- a/engine/namegen.mli
+++ b/engine/namegen.mli
@@ -125,7 +125,3 @@ val rename_bound_vars_as_displayed :
 val compute_displayed_name_in_gen :
   (evar_map -> int -> 'a -> bool) ->
   evar_map -> Id.Set.t -> Name.t -> 'a -> Name.t * Id.Set.t
-
-val set_mangle_names_mode : Id.t -> unit
-(** Turn on mangled names mode and with the given prefix.
-    @raise UserError if the argument is invalid as an identifier. *)
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index 68c2724f26..e20055b133 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -12,17 +12,12 @@ open Univ
 open UnivSubst
 
 (* To disallow minimization to Set *)
-let set_minimization = ref true
-let is_set_minimization () = !set_minimization
-
-let () =
-  Goptions.(declare_bool_option
-          { optdepr  = false;
-            optname  = "minimization to Set";
-            optkey   = ["Universe";"Minimization";"ToSet"];
-            optread  = is_set_minimization;
-            optwrite = (:=) set_minimization })
-
+let get_set_minimization =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~name:"minimization to Set"
+    ~key:["Universe";"Minimization";"ToSet"]
+    ~value:true
 
 (** Simplification *)
 
@@ -278,7 +273,7 @@ let normalize_context_set g ctx us algs weak =
   let smallles, csts =
     Constraint.partition (fun (l,d,r) -> d == Le && Level.is_small l) csts
   in
-  let smallles = if is_set_minimization ()
+  let smallles = if get_set_minimization ()
     then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx) smallles
     else Constraint.empty
   in
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 07ed7825ff..3a4969a3ee 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -604,15 +604,6 @@ let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function
      CErrors.user_err ?loc ~hdr:"coerce_to_cases_pattern_expr"
                       (str "This expression should be coercible to a pattern.")) c
 
-let asymmetric_patterns = ref (false)
-let () = Goptions.(declare_bool_option {
-  optdepr = false;
-  optname = "no parameters in constructors";
-  optkey = ["Asymmetric";"Patterns"];
-  optread = (fun () -> !asymmetric_patterns);
-  optwrite = (fun a -> asymmetric_patterns:=a);
-})
-
 (** Local universe and constraint declarations. *)
 
 let interp_univ_constraints env evd cstrs =
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 9e83bde8b2..7f14eb4583 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -127,9 +127,6 @@ val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> notation -
 (** For cases pattern parsing errors *)
 val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a
 
-(** Placeholder for global option, should be moved to a parameter *)
-val asymmetric_patterns : bool ref
-
 (** Local universe and constraint declarations. *)
 val interp_univ_decl : Environ.env -> universe_decl_expr ->
                        Evd.evar_map * UState.universe_decl
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 0f5fa14c23..25f2526f74 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -193,17 +193,12 @@ let without_specific_symbols l =
 (* Control printing of records *)
 
 (* Set Record Printing flag *)
-let record_print = ref true
-
-let () =
-  let open Goptions in
-  declare_bool_option
-    { optdepr  = false;
-      optname  = "record printing";
-      optkey   = ["Printing";"Records"];
-      optread  = (fun () -> !record_print);
-      optwrite = (fun b -> record_print := b) }
-
+let get_record_print =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~name:"record printing"
+    ~key:["Printing";"Records"]
+    ~value:true
 
 let is_record indsp =
   try
@@ -431,7 +426,7 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
 	    with
 		Not_found | No_match | Exit ->
                   let c = extern_reference Id.Set.empty (ConstructRef cstrsp) in
-                  if !asymmetric_patterns then
+                  if Constrintern.get_asymmetric_patterns () then
 		    if pattern_printable_in_both_syntax cstrsp
 		    then CPatCstr (c, None, args)
 		    else CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), [])
@@ -469,7 +464,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
 		List.map (extern_cases_pattern_in_scope subscope vars) c)
 		substlist in
 	    let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in
-            let l2' = if !asymmetric_patterns || not (List.is_empty ll) then l2
+            let l2' = if Constrintern.get_asymmetric_patterns () || not (List.is_empty ll) then l2
 	      else
 		match drop_implicits_in_patt gr nb_to_drop l2 with
 		  |Some true_args -> true_args
@@ -489,7 +484,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
           extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes)) vars c)
           subst in
       let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in
-      let l2' = if !asymmetric_patterns then l2
+      let l2' = if Constrintern.get_asymmetric_patterns () then l2
 	else
 	  match drop_implicits_in_patt gr (nb_to_drop + List.length l1) l2 with
 	    |Some true_args -> true_args
@@ -824,7 +819,7 @@ let rec extern inctx scopes vars r =
                    ()
                  else if PrintingConstructor.active (fst cstrsp) then
                    raise Exit
-                 else if not !record_print then
+                 else if not (get_record_print ()) then
                    raise Exit;
 		 let projs = struc.Recordops.s_PROJ in
 		 let locals = struc.Recordops.s_PROJKIND in
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 02db8f6aab..6313f2d7ba 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1488,6 +1488,12 @@ let is_non_zero_pat c = match c with
 | { CAst.v = CPatPrim (Numeral (p, true)) } -> not (is_zero p)
 | _ -> false
 
+let get_asymmetric_patterns = Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~name:"no parameters in constructors"
+    ~key:["Asymmetric";"Patterns"]
+    ~value:false
+
 let drop_notations_pattern looked_for genv =
   (* At toplevel, Constructors and Inductives are accepted, in recursive calls
      only constructor are allowed *)
@@ -1562,7 +1568,7 @@ let drop_notations_pattern looked_for genv =
 	| None -> DAst.make ?loc @@ RCPatAtom None
 	| Some (n, head, pl) ->
           let pl =
-            if !asymmetric_patterns then pl else
+            if get_asymmetric_patterns () then pl else
             let pars = List.make n (CAst.make ?loc @@ CPatAtom None) in
             List.rev_append pars pl in
 	  match drop_syndef top scopes head pl with
@@ -1684,7 +1690,7 @@ let rec intern_pat genv ntnvars aliases pat =
       let aliases' = merge_aliases aliases id in
       intern_pat genv ntnvars aliases' p
     | RCPatCstr (head, expl_pl, pl) ->
-      if !asymmetric_patterns then
+      if get_asymmetric_patterns () then
         let len = if List.is_empty expl_pl then Some (List.length pl) else None in
 	let c,idslpl1 = find_constructor loc len head in
 	let with_letin =
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 147a903fe2..035e4bc644 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -197,3 +197,6 @@ val parsing_explicit : bool ref
 
 (** Globalization leak for Grammar *)
 val for_grammar : ('a -> 'b) -> 'a -> 'b
+
+(** Placeholder for global option, should be moved to a parameter *)
+val get_asymmetric_patterns : unit -> bool
diff --git a/library/goptions.ml b/library/goptions.ml
index bb9b4e29fc..98efb512ab 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -299,6 +299,18 @@ let declare_stringopt_option =
     (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option."))
     (fun _ _ -> anomaly (Pp.str "async_option."))
 
+let declare_bool_option_and_ref ~depr ~name ~key ~(value:bool) =
+  let r_opt = ref value in
+  let optwrite v = r_opt := v in
+  let optread () = !r_opt in
+  let _ = declare_bool_option {
+      optdepr = depr;
+      optname = name;
+      optkey = key;
+      optread; optwrite
+    } in
+  optread
+
 (* 3- User accessible commands *)
 
 (* Setting values of options *)
@@ -422,6 +434,3 @@ let print_tables () =
       (fun (nickkey,_) p -> p ++ str "  " ++ str nickkey ++ fnl ())
       !ref_table (mt ()) ++
     fnl ()
-
-
-
diff --git a/library/goptions.mli b/library/goptions.mli
index 900217e06b..b91553bf3c 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -131,6 +131,9 @@ val declare_string_option: ?preprocess:(string -> string) ->
 val declare_stringopt_option: ?preprocess:(string option -> string option) ->
                               string option option_sig -> unit
 
+(** Helper to declare a reference controlled by an option. Read-only
+   as to avoid races. *)
+val declare_bool_option_and_ref : depr:bool -> name:string -> key:option_name -> value:bool -> (unit -> bool)
 
 (** {6 Special functions supposed to be used only in vernacentries.ml } *)
 
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 7104b8586e..f8289f558c 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -183,14 +183,11 @@ let cofixp_reducible flgs _ stk =
   else
     false
 
-let debug_cbv = ref false
-let () = Goptions.(declare_bool_option {
-  optdepr = false;
-  optname = "cbv visited constants display";
-  optkey = ["Debug";"Cbv"];
-  optread = (fun () -> !debug_cbv);
-  optwrite = (fun a -> debug_cbv:=a);
-})
+let get_debug_cbv = Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~value:false
+    ~name:"cbv visited constants display"
+    ~key:["Debug";"Cbv"]
 
 let debug_pr_key = function
   | ConstKey (sp,_) -> Names.Constant.print sp
@@ -325,14 +322,14 @@ and norm_head_ref k info env stack normt =
   if red_set_ref info.reds normt then
     match cbv_value_cache info normt with
       | Some body ->
-         if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ debug_pr_key normt);
+         if get_debug_cbv () then Feedback.msg_debug Pp.(str "Unfolding " ++ debug_pr_key normt);
          strip_appl (shift_value k body) stack
       | None ->
-         if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt);
+         if get_debug_cbv () then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt);
          (VAL(0,make_constr_ref k normt),stack)
   else
     begin
-      if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt);
+      if get_debug_cbv () then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt);
       (VAL(0,make_constr_ref k normt),stack)
     end
 
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 1edcc499f0..f18040accb 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -398,16 +398,12 @@ let class_params = function
 let add_class cl =
   add_new_class cl { cl_param = class_params cl }
 
-let automatically_import_coercions = ref false
-
-open Goptions
-let () =
-  declare_bool_option
-    { optdepr  = true; (* remove in 8.8 *)
-      optname  = "automatic import of coercions";
-      optkey   = ["Automatic";"Coercions";"Import"];
-      optread  = (fun () -> !automatically_import_coercions);
-      optwrite = (:=) automatically_import_coercions }
+let get_automatically_import_coercions =
+  Goptions.declare_bool_option_and_ref
+    ~depr:true (* Remove in 8.8 *)
+    ~name:"automatic import of coercions"
+    ~key:["Automatic";"Coercions";"Import"]
+    ~value:false
 
 let cache_coercion (_, c) =
   let () = add_class c.coercion_source in
@@ -425,7 +421,7 @@ let cache_coercion (_, c) =
   add_coercion_in_graph (xf,is,it)
 
 let load_coercion _ o =
-  if !automatically_import_coercions then
+  if get_automatically_import_coercions () then
     cache_coercion o
 
 let set_coercion_in_scope (_, c) =
@@ -435,7 +431,7 @@ let set_coercion_in_scope (_, c) =
 let open_coercion i o =
   if Int.equal i 1 then begin
     set_coercion_in_scope o;
-    if not !automatically_import_coercions then
+    if not (get_automatically_import_coercions ()) then
       cache_coercion o
   end
 
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 30eb70d0e7..4d1d405bd7 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -33,16 +33,12 @@ open Evd
 open Termops
 open Globnames
 
-let use_typeclasses_for_conversion = ref true
-
-let () =
-  Goptions.(declare_bool_option
-    { optdepr  = false;
-      optname  = "use typeclass resolution during conversion";
-      optkey   = ["Typeclass"; "Resolution"; "For"; "Conversion"];
-      optread  = (fun () -> !use_typeclasses_for_conversion);
-      optwrite = (fun b -> use_typeclasses_for_conversion := b) }
-    )
+let get_use_typeclasses_for_conversion =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~name:"use typeclass resolution during conversion"
+    ~key:["Typeclass"; "Resolution"; "For"; "Conversion"]
+    ~value:true
 
 (* Typing operations dealing with coercions *)
 exception NoCoercion
@@ -424,7 +420,7 @@ let inh_app_fun resolve_tc env evd j =
   try inh_app_fun_core env evd j
   with
   | NoCoercion when not resolve_tc
-    || not !use_typeclasses_for_conversion -> (evd, j)
+    || not (get_use_typeclasses_for_conversion ()) -> (evd, j)
   | NoCoercion ->
     try inh_app_fun_core env (saturate_evd env evd) j
     with NoCoercion -> (evd, j)
@@ -534,7 +530,7 @@ let inh_conv_coerce_to_gen ?loc resolve_tc rigidonly env evd cj t =
 	  coerce_itf ?loc env evd (Some cj.uj_val) cj.uj_type t
 	else raise NoSubtacCoercion
       with
-      | NoSubtacCoercion when not resolve_tc || not !use_typeclasses_for_conversion ->
+      | NoSubtacCoercion when not resolve_tc || not (get_use_typeclasses_for_conversion ()) ->
 	  error_actual_type ?loc env best_failed_evd cj t e
       | NoSubtacCoercion ->
 	let evd' = saturate_evd env evd in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 3391750209..f5e48bcd39 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -105,16 +105,12 @@ let search_guard ?loc env possible_indexes fixdefs =
 
 (* To force universe name declaration before use *)
 
-let strict_universe_declarations = ref true
-let is_strict_universe_declarations () = !strict_universe_declarations
-
-let () =
-  Goptions.(declare_bool_option
-	  { optdepr  = false;
-	    optname  = "strict universe declaration";
-	    optkey   = ["Strict";"Universe";"Declaration"];
-	    optread  = is_strict_universe_declarations;
-	    optwrite = (:=) strict_universe_declarations })
+let is_strict_universe_declarations =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~name:"strict universe declaration"
+    ~key:["Strict";"Universe";"Declaration"]
+    ~value:true
 
 (** Miscellaneous interpretation functions *)
 
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index c68890a87f..18c9650bd1 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -31,19 +31,12 @@ type 'a hint_info_gen =
 
 type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen
 
-let typeclasses_unique_solutions = ref false
-let set_typeclasses_unique_solutions d = (:=) typeclasses_unique_solutions d
-let get_typeclasses_unique_solutions () = !typeclasses_unique_solutions
-
-open Goptions
-
-let () =
-  declare_bool_option
-    { optdepr  = false;
-      optname  = "check that typeclasses proof search returns unique solutions";
-      optkey   = ["Typeclasses";"Unique";"Solutions"];
-      optread  = get_typeclasses_unique_solutions;
-      optwrite = set_typeclasses_unique_solutions; }
+let get_typeclasses_unique_solutions =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~name:"check that typeclasses proof search returns unique solutions"
+    ~key:["Typeclasses";"Unique";"Solutions"]
+    ~value:false
 
 let (add_instance_hint, add_instance_hint_hook) = Hook.make ()
 let add_instance_hint id = Hook.get add_instance_hint id
diff --git a/stm/stm.ml b/stm/stm.ml
index c078dbae56..94405924b7 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2838,13 +2838,12 @@ let process_back_meta_command ~newtip ~head oid aast w =
     VCS.commit id (Alias (oid,aast));
     Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
 
-let allow_nested_proofs = ref false
-let () = Goptions.(declare_bool_option
-    { optdepr  = false;
-      optname  = "Nested Proofs Allowed";
-      optkey   = Vernac_classifier.stm_allow_nested_proofs_option_name;
-      optread  = (fun () -> !allow_nested_proofs);
-      optwrite = (fun b -> allow_nested_proofs := b) })
+let get_allow_nested_proofs =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~name:"Nested Proofs Allowed"
+    ~key:Vernac_classifier.stm_allow_nested_proofs_option_name
+    ~value:false
 
 let process_transaction ~doc ?(newtip=Stateid.fresh ())
   ({ verbose; loc; expr } as x) c =
@@ -2877,7 +2876,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
       (* Proof *)
       | VtStartProof (mode, guarantee, names), w ->
 
-         if not !allow_nested_proofs && VCS.proof_nesting () > 0 then
+         if not (get_allow_nested_proofs ()) && VCS.proof_nesting () > 0 then
            "Nested proofs are not allowed unless you turn option Nested Proofs Allowed on."
            |> Pp.str
            |> (fun s -> (UserError (None, s), Exninfo.null))
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index b98535b201..191cc94e2b 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -281,11 +281,6 @@ let get_cache opt = function
   | "force" -> Some Stm.AsyncOpts.Force
   | _ -> prerr_endline ("Error: force expected after "^opt); exit 1
 
-let get_identifier opt s =
-  try Names.Id.of_string s
-  with CErrors.UserError _ ->
-    prerr_endline ("Error: valid identifier expected after option "^opt); exit 1
-
 let is_not_dash_option = function
   | Some f when String.length f > 0 && f.[0] <> '-' -> true
   | _ -> false
@@ -478,7 +473,9 @@ let parse_args arglist : coq_cmdopts * string list =
       add_load_vernacular oval true (next ())
 
     |"-mangle-names" ->
-      Namegen.set_mangle_names_mode (get_identifier opt (next ())); oval
+      Goptions.set_bool_option_value ["Mangle"; "Names"] true;
+      Goptions.set_string_option_value ["Mangle"; "Names"; "Prefix"] (next ());
+      oval
 
     |"-print-mod-uid" ->
       let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0
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";