diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index cd30eaf5ca..88b78a633f 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -997,7 +997,7 @@ let vernac_set_opacity local str = let vernac_set_option locality key = function | StringValue s -> set_string_option_value_gen locality key s - | IntValue n -> set_int_option_value_gen locality key (Some n) + | IntValue n -> set_int_option_value_gen locality key n | BoolValue b -> set_bool_option_value_gen locality key b let vernac_unset_option locality key = diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 32ea70baf2..bae6cfcdd9 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -134,10 +134,10 @@ type onlyparsing_flag = bool (* true = Parse only; false = Print also *) type infer_flag = bool (* true = try to Infer record; false = nothing *) type full_locality_flag = bool option (* true = Local; false = Global *) -type option_value = - | StringValue of string - | IntValue of int +type option_value = Goptions.option_value = | BoolValue of bool + | IntValue of int option + | StringValue of string type option_ref_value = | StringRefValue of string |