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 /pretyping/cbv.ml | |
| parent | 264aba2484312a2172cd36dd9b89ed66e4f38864 (diff) | |
Infrastructure for fine-grained debug flags
Diffstat (limited to 'pretyping/cbv.ml')
| -rw-r--r-- | pretyping/cbv.ml | 11 |
1 files changed, 4 insertions, 7 deletions
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 7930c3d634..02fb347d08 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -201,10 +201,7 @@ let cofixp_reducible flgs _ stk = else false -let get_debug_cbv = Goptions.declare_bool_option_and_ref - ~depr:false - ~value:false - ~key:["Debug";"Cbv"] +let debug_cbv = CDebug.create ~name:"Cbv" () (* Reduction of primitives *) @@ -525,7 +522,7 @@ and norm_head_ref k info env stack normt t = if red_set_ref info.reds normt then match cbv_value_cache info normt with | Declarations.Def body -> - if get_debug_cbv () then Feedback.msg_debug Pp.(str "Unfolding " ++ debug_pr_key normt); + debug_cbv (fun () -> Pp.(str "Unfolding " ++ debug_pr_key normt)); strip_appl (shift_value k body) stack | Declarations.Primitive op -> let c = match normt with @@ -534,11 +531,11 @@ and norm_head_ref k info env stack normt t = in (PRIMITIVE(op,c,[||]),stack) | Declarations.OpaqueDef _ | Declarations.Undef _ -> - if get_debug_cbv () then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt); + debug_cbv (fun () -> Pp.(str "Not unfolding " ++ debug_pr_key normt)); (VAL(0,make_constr_ref k normt t),stack) else begin - if get_debug_cbv () then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt); + debug_cbv (fun () -> Pp.(str "Not unfolding " ++ debug_pr_key normt)); (VAL(0,make_constr_ref k normt t),stack) end |