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 /library | |
| parent | 264aba2484312a2172cd36dd9b89ed66e4f38864 (diff) | |
Infrastructure for fine-grained debug flags
Diffstat (limited to 'library')
| -rw-r--r-- | library/nametab.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/nametab.ml b/library/nametab.ml index e94b696b60..bd96446f1c 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -574,7 +574,7 @@ let pr_global_env env ref = try pr_qualid (shortest_qualid_of_global env ref) with Not_found as exn -> let exn, info = Exninfo.capture exn in - if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found"); + if CDebug.(get_flag misc) then Feedback.msg_debug (Pp.str "pr_global_env not found"); Exninfo.iraise (exn, info) let global_inductive qid = |