From 40479227cba680496bf358e196e57a9a64f9c65b Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sun, 20 Sep 2015 00:58:25 +0200
Subject: Nametab: print debug notice only in debug mode.

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

diff --git a/library/nametab.ml b/library/nametab.ml
index 6af1e686b0..5b6d7cd982 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -524,7 +524,8 @@ let shortest_qualid_of_tactic kn =
 
 let pr_global_env env ref =
   try str (string_of_qualid (shortest_qualid_of_global env ref))
-  with Not_found as e -> prerr_endline "pr_global_env not found"; raise e
+  with Not_found as e ->
+    if !Flags.debug then Pp.msg_debug (Pp.str "pr_global_env not found"); raise e
 
 let global_inductive r =
   match global r with
-- 
cgit v1.2.3