From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 library/nametab.ml | 23 +++++++++++++----------
 1 file changed, 13 insertions(+), 10 deletions(-)

(limited to 'library/nametab.ml')

diff --git a/library/nametab.ml b/library/nametab.ml
index 40acb3ae..fa5db37e 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Pp
 open Names
@@ -82,6 +82,14 @@ module Make (U : UserName) (E : EqualityType) : NAMETREE
 struct
   type elt = E.t
 
+  (* A name became inaccessible, even with absolute qualification.
+     Example:
+     Module F (X : S). Module X.
+     The argument X of the functor F is masked by the inner module X.
+   *)
+  let masking_absolute n =
+    Flags.if_verbose Feedback.msg_info (str ("Trying to mask the absolute name \"" ^ U.to_string n ^ "\"!"))
+
   type user_name = U.t
 
   type path_status =
@@ -119,9 +127,7 @@ struct
 	      | Absolute (n,_) ->
 		  (* This is an absolute name, we must keep it
 		     otherwise it may become unaccessible forever *)
-		    msg_warning (str ("Trying to mask the absolute name \""
-			     ^ U.to_string n ^ "\"!"));
-		  tree.path
+                masking_absolute n; tree.path
 	      | Nothing
 	      | Relative _ -> Relative (uname,o)
           else tree.path
@@ -144,7 +150,6 @@ struct
 	  | Nothing
 	  | Relative _ -> mktree (Absolute (uname,o)) tree.map
 
-
 let rec push_exactly uname o level tree = function
 | [] ->
   anomaly (Pp.str "Prefix longer than path! Impossible!")
@@ -155,9 +160,7 @@ let rec push_exactly uname o level tree = function
         | Absolute (n,_) ->
             (* This is an absolute name, we must keep it
                 otherwise it may become unaccessible forever *)
-              msg_warning (str ("Trying to mask the absolute name \""
-                        ^ U.to_string n ^ "\"!"));
-            tree.path
+            masking_absolute n; tree.path
         | Nothing
         | Relative _ -> Relative (uname,o)
     in
@@ -523,9 +526,9 @@ let shortest_qualid_of_tactic kn =
     KnTab.shortest_qualid Id.Set.empty sp !the_tactictab
 
 let pr_global_env env ref =
-  try str (string_of_qualid (shortest_qualid_of_global env ref))
+  try pr_qualid (shortest_qualid_of_global env ref)
   with Not_found as e ->
-    if !Flags.debug then Pp.msg_debug (Pp.str "pr_global_env not found"); raise e
+    if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found"); raise e
 
 let global_inductive r =
   match global r with
-- 
cgit v1.2.3