diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index c07c756c0..5147d81bc 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1497,6 +1497,8 @@ let vernac_set_opacity locality (v,l) = let vernac_set_option locality key = function | 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 |