aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--sysinit/coqargs.ml5
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;