diff options
Diffstat (limited to 'library/nametab.ml')
| -rw-r--r-- | library/nametab.ml | 17 |
1 files changed, 7 insertions, 10 deletions
diff --git a/library/nametab.ml b/library/nametab.ml index f533bc7914..db902d625b 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -82,14 +82,6 @@ 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 = @@ -127,7 +119,9 @@ struct | Absolute (n,_) -> (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) - masking_absolute n; tree.path + Feedback.msg_warning (str ("Trying to mask the absolute name \"" + ^ U.to_string n ^ "\"!")); + tree.path | Nothing | Relative _ -> Relative (uname,o) else tree.path @@ -150,6 +144,7 @@ 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!") @@ -160,7 +155,9 @@ 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 *) - masking_absolute n; tree.path + Feedback.msg_warning (str ("Trying to mask the absolute name \"" + ^ U.to_string n ^ "\"!")); + tree.path | Nothing | Relative _ -> Relative (uname,o) in |