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

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

3 files changed, 15 insertions, 31 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