diff options
| author | Pierre-Marie Pédrot | 2020-03-12 15:31:26 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-18 11:57:19 +0100 |
| commit | d583f810be066929301864765601ff53497bc335 (patch) | |
| tree | 34ca12836c91fef1af681fec92b6ab45201c6b02 /vernac | |
| parent | 96ec58df041dc0111df0e681269aed9d0e9b571a (diff) | |
Export the user-facing attribute for hint locality.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/attributes.ml | 10 | ||||
| -rw-r--r-- | vernac/attributes.mli | 1 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 15 |
3 files changed, 23 insertions, 3 deletions
diff --git a/vernac/attributes.ml b/vernac/attributes.ml index 7213ba4829..96f126503d 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -163,6 +163,16 @@ let program = let locality = bool_attribute ~name:"Locality" ~on:"local" ~off:"global" +let option_locality = + let name = "Locality" in + attribute_of_list [ + ("local", single_key_parser ~name ~key:"local" Goptions.OptLocal); + ("global", single_key_parser ~name ~key:"global" Goptions.OptGlobal); + ("export", single_key_parser ~name ~key:"export" Goptions.OptExport); + ] >>= function + | None -> return Goptions.OptDefault + | Some l -> return l + let ukey = "universes" let universe_polymorphism_option_name = ["Universe"; "Polymorphism"] diff --git a/vernac/attributes.mli b/vernac/attributes.mli index 7ecb7e4fb0..660652081f 100644 --- a/vernac/attributes.mli +++ b/vernac/attributes.mli @@ -47,6 +47,7 @@ val polymorphic : bool attribute val program : bool attribute val template : bool option attribute val locality : bool option attribute +val option_locality : Goptions.option_locality attribute val deprecation : Deprecation.t option attribute val canonical_field : bool attribute val canonical_instance : bool attribute diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index c4027c6598..ba6d869589 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1178,9 +1178,18 @@ let vernac_hints ~atts dbnames h = (warn_implicit_core_hint_db (); ["core"]) else dbnames in - let local, poly = Attributes.(parse Notations.(locality ++ polymorphic) atts) in - let local = enforce_module_locality local in - let locality = if local then OptLocal else OptGlobal in + let locality, poly = Attributes.(parse Notations.(option_locality ++ polymorphic) atts) in + let () = match locality with + | 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 | OptLocal -> () + in Hints.add_hints ~locality dbnames (Hints.interp_hints ~poly h) let vernac_syntactic_definition ~atts lid x only_parsing = |