diff options
| author | Pierre-Marie Pédrot | 2020-11-13 19:42:54 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-16 12:28:27 +0100 |
| commit | 7daf04e53bdee6b0c9d0171c1e0d05903d677d3a (patch) | |
| tree | 4fce486f1c3d04045c0b925f788a8933920202c6 | |
| parent | 57fb6f106f24d2fa1e66a8ac813525f804a7ced7 (diff) | |
Warning on hint commands that have no explicit locality.
| -rw-r--r-- | vernac/vernacentries.ml | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 761f6ef5b7..4e52af7959 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1314,6 +1314,14 @@ let warn_implicit_core_hint_db = (fun () -> strbrk "Adding and removing hints in the core database implicitly is deprecated. " ++ strbrk"Please specify a hint database.") +let warn_deprecated_hint_without_locality = + CWarnings.create ~name:"deprecated-hint-without-locality" ~category:"deprecated" + (fun () -> strbrk "The default value for hint locality is currently \ + \"local\" in a section and \"global\" otherwise, but is scheduled to change \ + in a future release. For the time being, adding hints outside of sections \ + without specifying an explicit locality is therefore deprecated. It is \ + recommended to use \"export\" whenever possible.") + let check_hint_locality = function | OptGlobal -> if Global.sections_are_opened () then @@ -1323,7 +1331,10 @@ let check_hint_locality = function if Global.sections_are_opened () then CErrors.user_err Pp.(str "This command does not support the export attribute in sections."); -| OptDefault | OptLocal -> () +| OptDefault -> + if not @@ Global.sections_are_opened () then + warn_deprecated_hint_without_locality () +| OptLocal -> () let vernac_remove_hints ~atts dbnames ids = let locality = Attributes.(parse option_locality atts) in |