diff options
| author | coqbot-app[bot] | 2020-11-16 16:26:41 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-16 16:26:41 +0000 |
| commit | af96434d2991b9f01f6cd3963ed114b57e40792f (patch) | |
| tree | d10e879b4d7ae13c3623fd7073631e219f24753b /vernac | |
| parent | a400dbf104ea3bf0fef51a62e774fb4ff60a7397 (diff) | |
| parent | 4f28dd46d4bfce732693d6904f80e25b53d4fb2a (diff) | |
Merge PR #13384: Warn on hints without an explicit locality
Reviewed-by: Zimmi48
Diffstat (limited to 'vernac')
| -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 |