aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2017-11-30 09:58:18 +0100
committerGravatar Matthieu Sozeau <mattam@mattam.org>2017-11-30 09:59:10 +0100
commite4f04163d1e7c901fca1030569f8ca9d95ee4d98 (patch)
treee1c757f0b9196ad71bb7af99de6d3b6d2e396aad /library
parentf303ed9fb26797b9ec7d172fe583e7ee607ae441 (diff)
Warning for absolute name masking (making it deprecated, should become
an error)
Diffstat (limited to 'library')
-rw-r--r--library/nametab.ml9
1 files changed, 5 insertions, 4 deletions
diff --git a/library/nametab.ml b/library/nametab.ml
index 0ec4a37cd..861d5f27f 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