diff options
| author | Maxime Dénès | 2020-10-15 15:31:51 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2021-02-24 15:09:15 +0100 |
| commit | 068031ff7da092c1e2d35db27d713b9606960c42 (patch) | |
| tree | 2a3e2ae6a82e60a76ef31659ff305d70a4b2ea39 /tactics | |
| parent | 264aba2484312a2172cd36dd9b89ed66e4f38864 (diff) | |
Infrastructure for fine-grained debug flags
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/cbn.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/tactics/cbn.ml b/tactics/cbn.ml index 6fb6cff04f..167f7d4026 100644 --- a/tactics/cbn.ml +++ b/tactics/cbn.ml @@ -562,19 +562,18 @@ 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 () = debug_RAKAM (fun () -> let open Pp in let pr c = Termops.Internal.print_constr_env env sigma c in - Feedback.msg_debug (h (str "<<" ++ pr x ++ str "|" ++ cut () ++ Cst_stack.pr env sigma cst_l ++ 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 () -> + Pp.(str "<><><><><>")) in ((EConstr.of_kind c0, stack),cst_l) in match c0 with |