diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-18 18:59:12 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-18 18:59:12 +0100 |
| commit | 015c9549d15e236f653b528747c1c528eff26e3c (patch) | |
| tree | 8f2922980353f648dd566fab545e3d7eaeb31757 /library/nametab.ml | |
| parent | 9266d34a073859f24aa615767a1311d532bba0ac (diff) | |
| parent | e4f04163d1e7c901fca1030569f8ca9d95ee4d98 (diff) | |
Merge PR #6284: Warning for absolute name masking (deprecated, should become an error)
Diffstat (limited to 'library/nametab.ml')
| -rw-r--r-- | library/nametab.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/library/nametab.ml b/library/nametab.ml index 84225f863..08881d6d7 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -81,8 +81,9 @@ struct 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 ^ "\"!")) + let warn_masking_absolute = + CWarnings.create ~name:"masking-absolute-name" ~category:"deprecated" + (fun n -> str ("Trying to mask the absolute name \"" ^ U.to_string n ^ "\"!")) type user_name = U.t @@ -121,7 +122,7 @@ struct | Absolute (n,_) -> (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) - masking_absolute n; tree.path + warn_masking_absolute n; tree.path | Nothing | Relative _ -> Relative (uname,o) else tree.path @@ -154,7 +155,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 *) - masking_absolute n; tree.path + warn_masking_absolute n; tree.path | Nothing | Relative _ -> Relative (uname,o) in |