diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 16 |
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 |