diff options
Diffstat (limited to 'library/nametab.ml')
| -rw-r--r-- | library/nametab.ml | 23 |
1 files changed, 13 insertions, 10 deletions
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 |