Export the user-facing attribute for hint locality.

1 files changed, 10 insertions, 0 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"]