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

7 files changed, 118 insertions, 174 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 73be36d031..857918c928 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -221,53 +221,35 @@ module PrintingLet = Goptions.MakeRefTable(PrintingCasesLet)
 
 (* Flags.for printing or not wildcard and synthetisable types *)
 
-open Goptions
-
-let wildcard_value = ref true
-let force_wildcard () = !wildcard_value
-
-let () = declare_bool_option
-          { optdepr  = false;
-            optkey   = ["Printing";"Wildcard"];
-            optread  = force_wildcard;
-            optwrite = (:=) wildcard_value }
-
-let fast_name_generation = ref false
-
-let () = declare_bool_option {
-  optdepr = false;
-  optkey = ["Fast";"Name";"Printing"];
-  optread = (fun () -> !fast_name_generation);
-  optwrite = (:=) fast_name_generation;
-}
-
-let synth_type_value = ref true
-let synthetize_type () = !synth_type_value
-
-let () = declare_bool_option
-          { optdepr  = false;
-            optkey   = ["Printing";"Synth"];
-            optread  = synthetize_type;
-            optwrite = (:=) synth_type_value }
-
-let reverse_matching_value = ref true
-let reverse_matching () = !reverse_matching_value
-
-let () = declare_bool_option
-          { optdepr  = false;
-            optkey   = ["Printing";"Matching"];
-            optread  = reverse_matching;
-            optwrite = (:=) reverse_matching_value }
-
-let print_primproj_params_value = ref false
-let print_primproj_params () = !print_primproj_params_value
-
-let () = declare_bool_option
-          { optdepr  = false;
-            optkey   = ["Printing";"Primitive";"Projection";"Parameters"];
-            optread  = print_primproj_params;
-            optwrite = (:=) print_primproj_params_value }
-
+let force_wildcard =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Printing";"Wildcard"]
+    ~value:true
+
+let fast_name_generation =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Fast";"Name";"Printing"]
+    ~value:false
+
+let synthetize_type =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Printing";"Synth"]
+    ~value:true
+
+let reverse_matching =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Printing";"Matching"]
+    ~value:true
+
+let print_primproj_params =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Printing";"Primitive";"Projection";"Parameters"]
+    ~value:false
 
 (* Auxiliary function for MutCase printing *)
 (* [computable] tries to tell if the predicate typing the result is inferable*)
@@ -338,27 +320,23 @@ let lookup_index_as_renamed env sigma t n =
 (**********************************************************************)
 (* Factorization of match patterns *)
 
-let print_factorize_match_patterns = ref true
-
-let () =
-  declare_bool_option
-    { optdepr  = false;
-      optkey   = ["Printing";"Factorizable";"Match";"Patterns"];
-      optread  = (fun () -> !print_factorize_match_patterns);
-      optwrite = (fun b -> print_factorize_match_patterns := b) }
-
-let print_allow_match_default_clause = ref true
+let print_factorize_match_patterns =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Printing";"Factorizable";"Match";"Patterns"]
+    ~value:true
 
-let () =
-  declare_bool_option
-    { optdepr  = false;
-      optkey   = ["Printing";"Allow";"Match";"Default";"Clause"];
-      optread  = (fun () -> !print_allow_match_default_clause);
-      optwrite = (fun b -> print_allow_match_default_clause := b) }
+let print_allow_match_default_opt_name =
+  ["Printing";"Allow";"Match";"Default";"Clause"]
+let print_allow_match_default_clause =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:print_allow_match_default_opt_name
+    ~value:true
 
 let rec join_eqns (ids,rhs as x) patll = function
   | ({CAst.loc; v=(ids',patl',rhs')} as eqn')::rest ->
-     if not !Flags.raw_print && !print_factorize_match_patterns &&
+     if not !Flags.raw_print && print_factorize_match_patterns () &&
         List.eq_set Id.equal ids ids' && glob_constr_eq rhs rhs'
      then
        join_eqns x (patl'::patll) rest
@@ -404,7 +382,7 @@ let factorize_eqns eqns =
   let eqns = aux [] (List.rev eqns) in
   let mk_anon patl = List.map (fun _ -> DAst.make @@ PatVar Anonymous) patl in
   let open CAst in
-  if not !Flags.raw_print && !print_allow_match_default_clause && eqns <> [] then
+  if not !Flags.raw_print && print_allow_match_default_clause () && eqns <> [] then
     match select_default_clause eqns with
     (* At least two clauses and the last one is disjunctive with no variables *)
     | Some {loc=gloc;v=([],patl::_::_,rhs)}, (_::_ as eqns) ->
@@ -925,16 +903,16 @@ let detype_rel_context d flags where avoid env sigma sign =
 
 let detype_names isgoal avoid nenv env sigma t =
   let flags = { flg_isgoal = isgoal; flg_lax = false } in
-  let avoid = Avoid.make ~fast:!fast_name_generation avoid in
+  let avoid = Avoid.make ~fast:(fast_name_generation ()) avoid in
   detype Now flags avoid (nenv,env) sigma t
 let detype d ?(lax=false) isgoal avoid env sigma t =
   let flags = { flg_isgoal = isgoal; flg_lax = lax } in
-  let avoid = Avoid.make ~fast:!fast_name_generation avoid in
+  let avoid = Avoid.make ~fast:(fast_name_generation ()) avoid in
   detype d flags avoid (names_of_rel_context env, env) sigma t
 
 let detype_rel_context d ?(lax = false) where avoid env sigma sign =
   let flags = { flg_isgoal = false; flg_lax = lax } in
-  let avoid = Avoid.make ~fast:!fast_name_generation avoid in
+  let avoid = Avoid.make ~fast:(fast_name_generation ()) avoid in
   detype_rel_context d flags where avoid env sigma sign
 
 let detype_closed_glob ?lax isgoal avoid env sigma t =
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 5723b47715..254f772ff8 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -29,11 +29,12 @@ val print_evar_arguments : bool ref
 
 (** If true, contract branches with same r.h.s. and same matching
     variables in a disjunctive pattern *)
-val print_factorize_match_patterns : bool ref
+val print_factorize_match_patterns : unit -> bool
 
-(** If true and the last non unique clause of a "match" is a
+(** If this flag is true and the last non unique clause of a "match" is a
     variable-free disjunctive pattern, turn it into a catch-call case *)
-val print_allow_match_default_clause : bool ref
+val print_allow_match_default_clause : unit -> bool
+val print_allow_match_default_opt_name : string list
 
 val subst_cases_pattern : substitution -> cases_pattern -> cases_pattern
 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 26bf02aa25..3d887e1a95 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -47,21 +47,17 @@ let default_flags env =
   let ts = default_transparent_state env in
   default_flags_of ts
 
-let debug_unification = ref (false)
-let () = Goptions.(declare_bool_option {
-  optdepr = false;
-  optkey = ["Debug";"Unification"];
-  optread = (fun () -> !debug_unification);
-  optwrite = (fun a -> debug_unification:=a);
-})
-
-let debug_ho_unification = ref (false)
-let () = Goptions.(declare_bool_option {
-  optdepr = false;
-  optkey = ["Debug";"HO";"Unification"];
-  optread = (fun () -> !debug_ho_unification);
-  optwrite = (fun a -> debug_ho_unification:=a);
-})
+let debug_unification =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Debug";"Unification"]
+    ~value:false
+
+let debug_ho_unification =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Debug";"HO";"Unification"]
+    ~value:false
 
 (*******************************************)
 (* Functions to deal with impossible cases *)
@@ -767,7 +763,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
   in
   let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in
   (* Evar must be undefined since we have flushed evars *)
-  let () = if !debug_unification then
+  let () = if debug_unification () then
              let open Pp in
              Feedback.msg_debug (v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ())) in
   match (flex_kind_of_term flags env evd term1 sk1,
@@ -1224,16 +1220,16 @@ let apply_on_subterm env evd fixedref f test c t =
               (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c)))
               applyrec acc t
     else
-    (if !debug_ho_unification then
+    (if debug_ho_unification () then
      Feedback.msg_debug Pp.(str"Testing " ++ prc env !evdref c ++ str" against " ++ prc env !evdref t);
      let b, evd =
         try test env !evdref k c t
         with e when CErrors.noncritical e -> assert false in
-     if b then (if !debug_ho_unification then Feedback.msg_debug (Pp.str "succeeded");
+     if b then (if debug_ho_unification () then Feedback.msg_debug (Pp.str "succeeded");
                 let evd', t' = f !evdref k t in
                 evdref := evd'; t')
      else (
-       if !debug_ho_unification then Feedback.msg_debug (Pp.str "failed");
+       if debug_ho_unification () then Feedback.msg_debug (Pp.str "failed");
        map_constr_with_binders_left_to_right !evdref
         (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c)))
         applyrec acc t))
@@ -1337,7 +1333,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
   let env_evar = evar_filtered_env env_rhs evi in
   let sign = named_context_val env_evar in
   let ctxt = evar_filtered_context evi in
-  if !debug_ho_unification then
+  if debug_ho_unification () then
     (Feedback.msg_debug Pp.(str"env rhs: " ++ Termops.Internal.print_env env_rhs);
      Feedback.msg_debug Pp.(str"env evars: " ++ Termops.Internal.print_env env_evar));
   let args = Array.map (nf_evar evd) args in
@@ -1374,7 +1370,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
   let rec set_holes env_rhs evd rhs = function
   | (id,idty,c,cty,evsref,filter,occs)::subst ->
      let c = nf_evar evd c in
-     if !debug_ho_unification then
+     if debug_ho_unification () then
        Feedback.msg_debug Pp.(str"set holes for: " ++
                                 prc env_rhs evd (mkVar id.binder_name) ++ spc () ++
                                 prc env_rhs evd c ++ str" in " ++
@@ -1382,7 +1378,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
      let occ = ref 1 in
      let set_var evd k inst =
        let oc = !occ in
-       if !debug_ho_unification then
+       if debug_ho_unification () then
        (Feedback.msg_debug Pp.(str"Found one occurrence");
         Feedback.msg_debug Pp.(str"cty: " ++ prc env_rhs evd c));
        incr occ;
@@ -1393,7 +1389,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
        | Unspecified prefer_abstraction ->
           let evd, evty = set_holes env_rhs evd cty subst in
           let evty = nf_evar evd evty in
-          if !debug_ho_unification then
+          if debug_ho_unification () then
             Feedback.msg_debug Pp.(str"abstracting one occurrence " ++ prc env_rhs evd inst ++
                                    str" of type: " ++ prc env_evar evd evty ++
                                    str " for " ++ prc env_rhs evd c);
@@ -1413,7 +1409,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
           evd, ev
      in
      let evd, rhs' = apply_on_subterm env_rhs evd fixed set_var test c rhs in
-     if !debug_ho_unification then
+     if debug_ho_unification () then
        Feedback.msg_debug Pp.(str"abstracted: " ++ prc env_rhs evd rhs');
      let () = check_selected_occs env_rhs evd c !occ occs in
      let env_rhs' = push_named (NamedDecl.LocalAssum (id,idty)) env_rhs in
@@ -1427,7 +1423,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
   (* Thin evars making the term typable in env_evar *)
   let evd, rhs' = thin_evars env_evar evd ctxt rhs' in
   (* We instantiate the evars of which the value is forced by typing *)
-  if !debug_ho_unification then
+  if debug_ho_unification () then
     (Feedback.msg_debug Pp.(str"solve_evars on: " ++ prc env_evar evd rhs');
      Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) env_evar evd));
   let evd,rhs' =
@@ -1437,7 +1433,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
       raise (TypingFailed evd) in
   let rhs' = nf_evar evd rhs' in
   (* We instantiate the evars of which the value is forced by typing *)
-  if !debug_ho_unification then
+  if debug_ho_unification () then
     (Feedback.msg_debug Pp.(str"after solve_evars: " ++ prc env_evar evd rhs');
      Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) env_evar evd));
 
@@ -1445,7 +1441,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
    | (id,idty,c,cty,evsref,_,_)::l ->
      let id = id.binder_name in
      let c = nf_evar evd c in
-     if !debug_ho_unification then
+     if debug_ho_unification () then
        Feedback.msg_debug Pp.(str"abstracting: " ++
                                 prc env_rhs evd (mkVar id) ++ spc () ++
                                 prc env_rhs evd c);
@@ -1476,7 +1472,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
                | _ -> evd)
            with e -> user_err (Pp.str "Cannot find an instance")
          else
-           ((if !debug_ho_unification then
+           ((if debug_ho_unification () then
                let evi = Evd.find evd evk in
                let env = Evd.evar_env env_rhs evi in
                Feedback.msg_debug Pp.(str"evar is defined: " ++
@@ -1491,7 +1487,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
      if Evd.is_defined evd evk then
        (* Can happen due to dependencies: instantiating evars in the arguments of evk might
            instantiate evk itself. *)
-       (if !debug_ho_unification then
+       (if debug_ho_unification () then
           begin
             let evi = Evd.find evd evk in
             let evenv = evar_env env_rhs evi in
@@ -1504,13 +1500,13 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
          let evi = Evd.find_undefined evd evk in
          let evenv = evar_env env_rhs evi in
          let rhs' = nf_evar evd rhs' in
-           if !debug_ho_unification then
+           if debug_ho_unification () then
              Feedback.msg_debug Pp.(str"abstracted type before second solve_evars: " ++
                                       prc evenv evd rhs');
          (* solve_evars is not commuting with nf_evar, because restricting
              an evar might provide a more specific type. *)
           let evd, _ = !solve_evars evenv evd rhs' in
-          if !debug_ho_unification then
+          if debug_ho_unification () then
             Feedback.msg_debug Pp.(str"abstracted type: " ++ prc evenv evd (nf_evar evd rhs'));
           let flags = default_flags_of TransparentState.full in
             Evarsolve.instantiate_evar evar_unify flags env_rhs evd evk rhs'
@@ -1564,7 +1560,7 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 =
   let t2 = apprec_nohdbeta flags env evd (whd_head_evar evd t2) in
   let (term1,l1 as appr1) = try destApp evd t1 with DestKO -> (t1, [||]) in
   let (term2,l2 as appr2) = try destApp evd t2 with DestKO -> (t2, [||]) in
-  let () = if !debug_unification then
+  let () = if debug_unification () then
              let open Pp in
              Feedback.msg_debug (v 0 (str "Heuristic:" ++ spc () ++
                                 Termops.Internal.print_constr_env env evd t1 ++ cut () ++
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index f989dae4c9..c1ca40329a 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -28,16 +28,22 @@ exception Find_at of int
 
 (* timing *)
 
-let timing_enabled = ref false
+let get_timing_enabled =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["NativeCompute"; "Timing"]
+    ~value:false
 
 (* profiling *)
 
-let profiling_enabled = ref false
+let get_profiling_enabled =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["NativeCompute"; "Profiling"]
+    ~value:false
 
 (* for supported platforms, filename for profiler results *)
 
-let profile_filename = ref "native_compute_profile.data"
-
 let profiler_platform () =
   match [@warning "-8"] Sys.os_type with
   | "Unix" ->
@@ -48,10 +54,11 @@ let profiler_platform () =
   | "Win32" -> "Windows (Win32)"
   | "Cygwin" -> "Windows (Cygwin)"
 
-let get_profile_filename () = !profile_filename
-
-let set_profile_filename fn =
-  profile_filename := fn
+let get_profile_filename =
+  Goptions.declare_string_option_and_ref
+    ~depr:false
+    ~key:["NativeCompute"; "Profile"; "Filename"]
+    ~value:"native_compute_profile.data"
 
 (* find unused profile filename *)
 let get_available_profile_filename () =
@@ -77,18 +84,6 @@ let get_available_profile_filename () =
     let _ = Feedback.msg_info (Pp.str msg) in
     assert false
 
-let get_profiling_enabled () =
-  !profiling_enabled
-
-let set_profiling_enabled b =
-  profiling_enabled := b
-
-let get_timing_enabled () =
-  !timing_enabled
-
-let set_timing_enabled b =
-  timing_enabled := b
-
 let invert_tag cst tag reloc_tbl =
   try
     for j = 0 to Array.length reloc_tbl - 1 do
diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli
index 4f18174261..73a8add6ec 100644
--- a/pretyping/nativenorm.mli
+++ b/pretyping/nativenorm.mli
@@ -14,16 +14,6 @@ open Evd
 
 (** This module implements normalization by evaluation to OCaml code *)
 
-val get_profile_filename : unit -> string
-val set_profile_filename : string -> unit
-
-val get_profiling_enabled : unit -> bool
-val set_profiling_enabled : bool -> unit
-
-val get_timing_enabled : unit -> bool
-val set_timing_enabled : bool -> unit
-
-
 val native_norm : env -> evar_map -> constr -> types -> constr
 
 (** Conversion with inference of universe constraints *)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 01f3537a7f..f7456ef35e 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -30,14 +30,6 @@ exception Elimconst
     their parameters in its stack.
 *)
 
-let () = Goptions.(declare_bool_option {
-  optdepr = false;
-  optkey = ["Cumulativity";"Weak";"Constraints"];
-  optread = (fun () -> not !UState.drop_weak_constraints);
-  optwrite = (fun a -> UState.drop_weak_constraints:=not a);
-})
-
-
 (** Support for reduction effects *)
 
 open Mod_subst
@@ -966,13 +958,11 @@ module CredNative = RedNative(CNativeEntries)
     contract_* in any case .
 *)
 
-let debug_RAKAM = ref (false)
-let () = Goptions.(declare_bool_option {
-  optdepr = false;
-  optkey = ["Debug";"RAKAM"];
-  optread = (fun () -> !debug_RAKAM);
-  optwrite = (fun a -> debug_RAKAM:=a);
-})
+let debug_RAKAM =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Debug";"RAKAM"]
+    ~value:false
 
 let equal_stacks sigma (x, l) (y, l') =
   let f_equal x y = eq_constr sigma x y in
@@ -983,7 +973,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
   let open Context.Named.Declaration in
   let open ReductionBehaviour in
   let rec whrec cst_l (x, stack) =
-    let () = if !debug_RAKAM then
+    let () = if debug_RAKAM () then
         let open Pp in
         let pr c = Termops.Internal.print_constr_env env sigma c in
         Feedback.msg_debug
@@ -994,7 +984,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
     in
     let c0 = EConstr.kind sigma x in
     let fold () =
-      let () = if !debug_RAKAM then
+      let () = if debug_RAKAM () then
           let open Pp in Feedback.msg_debug (str "<><><><><>") in
       ((EConstr.of_kind c0, stack),cst_l)
     in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 90dde01915..e168f6d1b6 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -43,23 +43,17 @@ type subst0 =
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
-let keyed_unification = ref (false)
-let () = Goptions.(declare_bool_option {
-  optdepr = false;
-  optkey = ["Keyed";"Unification"];
-  optread = (fun () -> !keyed_unification);
-  optwrite = (fun a -> keyed_unification:=a);
-})
-
-let is_keyed_unification () = !keyed_unification
-
-let debug_unification = ref (false)
-let () = Goptions.(declare_bool_option {
-  optdepr = false;
-  optkey = ["Debug";"Tactic";"Unification"];
-  optread = (fun () -> !debug_unification);
-  optwrite = (fun a -> debug_unification:=a);
-})
+let is_keyed_unification =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Keyed";"Unification"]
+    ~value:false
+
+let debug_unification =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Debug";"Tactic";"Unification"]
+    ~value:false
 
 (** Making this unification algorithm correct w.r.t. the evar-map abstraction
     breaks too much stuff. So we redefine incorrect functions here. *)
@@ -702,7 +696,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
     let cM = Evarutil.whd_head_evar sigma curm
     and cN = Evarutil.whd_head_evar sigma curn in
     let () =
-      if !debug_unification then
+      if debug_unification () then
         Feedback.msg_debug (
           Termops.Internal.print_constr_env curenv sigma cM ++ str" ~= " ++
           Termops.Internal.print_constr_env curenv sigma cN)
@@ -1127,7 +1121,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
     else error_cannot_unify (fst curenvnb) sigma (cM,cN)
   in
 
-  if !debug_unification then Feedback.msg_debug (str "Starting unification");
+  if debug_unification () then Feedback.msg_debug (str "Starting unification");
   let opt = { at_top = conv_at_top; with_types = false; with_cs = true } in
   try
   let res =
@@ -1152,11 +1146,11 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
     let a = match res with
     | Some sigma -> sigma, ms, es
     | None -> unirec_rec (env,0) cv_pb opt subst m n in
-    if !debug_unification then Feedback.msg_debug (str "Leaving unification with success");
+    if debug_unification () then Feedback.msg_debug (str "Leaving unification with success");
     a
   with e ->
     let e = Exninfo.capture e in
-    if !debug_unification then Feedback.msg_debug (str "Leaving unification with failure");
+    if debug_unification () then Feedback.msg_debug (str "Leaving unification with failure");
     Exninfo.iraise e
 
 let unify_0 env sigma = unify_0_with_initial_metas (sigma,[],[]) true env
@@ -1745,7 +1739,7 @@ let make_abstraction env evd ccl abs =
         env evd c ty occs check_occs ccl
 
 let keyed_unify env evd kop =
-  if not !keyed_unification then fun cl -> true
+  if not (is_keyed_unification ()) then fun cl -> true
   else
     match kop with
     | None -> fun _ -> true
@@ -1767,7 +1761,7 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
     (try
        if closed0 evd cl && not (isEvar evd cl) && keyed_unify env evd kop cl then
        (try
-         if !keyed_unification then
+         if is_keyed_unification () then
            let f1, l1 = decompose_app_vect evd op in
            let f2, l2 = decompose_app_vect evd cl in
            w_typed_unify_array env evd flags f1 l1 f2 l2,cl
@@ -1913,7 +1907,7 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t =
       else
         let allow_K = flags.allow_K_in_toplevel_higher_order_unification in
         let flags =
-          if unsafe_occur_meta_or_existential op || !keyed_unification then
+          if unsafe_occur_meta_or_existential op || is_keyed_unification () then
             (* This is up to delta for subterms w/o metas ... *)
             flags
           else