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

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

5 files changed, 36 insertions, 58 deletions

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