diff options
Diffstat (limited to 'sysinit')
| -rw-r--r-- | sysinit/coqargs.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml index 19350b7e98..ac9e430d31 100644 --- a/sysinit/coqargs.ml +++ b/sysinit/coqargs.ml @@ -348,9 +348,8 @@ let parse_args ~usage ~init arglist : t * string list = add_load_vernacular oval true (next ()) |"-mangle-names" -> - Goptions.set_bool_option_value ["Mangle"; "Names"] true; - Goptions.set_string_option_value ["Mangle"; "Names"; "Prefix"] (next ()); - oval + let oval = add_set_option oval ["Mangle"; "Names"] (OptionSet None) in + add_set_option oval ["Mangle"; "Names"; "Prefix"] (OptionSet(Some(next ()))) |"-profile-ltac-cutoff" -> Flags.profile_ltac := true; |