diff options
| author | Gaëtan Gilbert | 2021-01-07 13:55:23 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2021-01-18 13:08:17 +0100 |
| commit | 4419a101a4f5a108be90cf4e420f0b6961e6caac (patch) | |
| tree | c3a3dcede7a5901685d28da3d540451e39c4b6f1 /vernac/vernacentries.ml | |
| parent | 58a4f645ee6d306cb824c2ac2dfa21e460b9692a (diff) | |
Support locality attributes for Hint Rewrite (including export)
We deprecate unspecified locality as was done for Hint.
Close #13724
Diffstat (limited to 'vernac/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 26 |
1 files changed, 2 insertions, 24 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 4f3fc46c12..1c774a35bf 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1401,31 +1401,9 @@ 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 - CErrors.user_err Pp.(str - "This command does not support the global attribute in sections."); -| OptExport -> - if Global.sections_are_opened () then - CErrors.user_err Pp.(str - "This command does not support the export attribute in sections."); -| 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 - let () = check_hint_locality locality in + let () = Hints.check_hint_locality locality in let dbnames = if List.is_empty dbnames then (warn_implicit_core_hint_db (); ["core"]) @@ -1440,7 +1418,7 @@ let vernac_hints ~atts dbnames h = else dbnames in let locality, poly = Attributes.(parse Notations.(option_locality ++ polymorphic) atts) in - let () = check_hint_locality locality in + let () = Hints.check_hint_locality locality in Hints.add_hints ~locality dbnames (ComHints.interp_hints ~poly h) let vernac_syntactic_definition ~atts lid x only_parsing = |