Merge PR #13202: Infrastructure for fine-grained debug flags

Reviewed-by: gares
Ack-by: herbelin
Ack-by: Zimmi48
Ack-by: jfehrle
Ack-by: SkySkimmer
Ack-by: ejgallego

1 files changed, 6 insertions, 10 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 54a47a252d..4083d3bc23 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -686,11 +686,7 @@ module CredNative = RedNative(CNativeEntries)
     contract_* in any case .
 *)
 
-let debug_RAKAM =
-  Goptions.declare_bool_option_and_ref
-    ~depr:false
-    ~key:["Debug";"RAKAM"]
-    ~value:false
+let debug_RAKAM = CDebug.create ~name:"RAKAM" ()
 
 let apply_branch env sigma (ind, i) args (ci, u, pms, iv, r, lf) =
   let args = Stack.tail ci.ci_npar args in
@@ -709,18 +705,18 @@ let apply_branch env sigma (ind, i) args (ci, u, pms, iv, r, lf) =
 let rec whd_state_gen flags env sigma =
   let open Context.Named.Declaration in
   let rec whrec (x, stack) : state =
-    let () = if debug_RAKAM () then
+    let () =
         let open Pp in
         let pr c = Termops.Internal.print_constr_env env sigma c in
-        Feedback.msg_debug
+        debug_RAKAM (fun () ->
                (h (str "<<" ++ pr x ++
                    str "|" ++ cut () ++ Stack.pr pr stack ++
-                   str ">>"))
+                   str ">>")))
     in
     let c0 = EConstr.kind sigma x in
     let fold () =
-      let () = if debug_RAKAM () then
-          let open Pp in Feedback.msg_debug (str "<><><><><>") in
+      let () = debug_RAKAM (fun () ->
+          let open Pp in str "<><><><><>") in
       ((EConstr.of_kind c0, stack))
     in
     match c0 with