From 068031ff7da092c1e2d35db27d713b9606960c42 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 15 Oct 2020 15:31:51 +0200
Subject: Infrastructure for fine-grained debug flags

---
 library/nametab.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library')

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 =
-- 
cgit v1.2.3