Export the various option localities in the API.

This prevents relying on an underspecified bool option argument.

1 files changed, 17 insertions, 8 deletions

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 4c9b41b21..3610e9da3 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1539,18 +1539,27 @@ let vernac_set_opacity ~atts (v,l) =
   let l = List.map glob_ref l in
   Redexpr.set_strategy local [v,l]
 
-let vernac_set_option ~atts key = function
-  | StringValue s -> set_string_option_value_gen atts.locality key s
-  | StringOptValue (Some s) -> set_string_option_value_gen atts.locality key s
-  | StringOptValue None -> unset_option_value_gen atts.locality key
-  | IntValue n -> set_int_option_value_gen atts.locality key n
-  | BoolValue b -> set_bool_option_value_gen atts.locality key b
+let get_option_locality = function
+| Some true -> OptLocal
+| Some false -> OptGlobal
+| None -> OptDefault
+
+let vernac_set_option ~atts key opt =
+  let locality = get_option_locality atts.locality in
+  match opt with
+  | StringValue s -> set_string_option_value_gen ~locality key s
+  | StringOptValue (Some s) -> set_string_option_value_gen ~locality key s
+  | StringOptValue None -> unset_option_value_gen ~locality key
+  | IntValue n -> set_int_option_value_gen ~locality key n
+  | BoolValue b -> set_bool_option_value_gen ~locality key b
 
 let vernac_set_append_option ~atts key s =
-  set_string_option_append_value_gen atts.locality key s
+  let locality = get_option_locality atts.locality in
+  set_string_option_append_value_gen ~locality key s
 
 let vernac_unset_option ~atts key =
-  unset_option_value_gen atts.locality key
+  let locality = get_option_locality atts.locality in
+  unset_option_value_gen ~locality key
 
 let vernac_add_option key lv =
   let f = function