diff options
| author | Emilio Jesus Gallego Arias | 2018-10-13 21:19:34 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-28 02:00:53 +0100 |
| commit | df85d9b765940b58a189b91cfdc67be7e0fd75e3 (patch) | |
| tree | 297517301041274f5546b5f62f7181c3cf70f2fc /toplevel | |
| parent | ec7aec452da1ad0bf53145a314df7c00194218a6 (diff) | |
[options] New helper for creation of boolean options plus reference.
This makes setting the option outside of the synchronized summary impossible.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqargs.ml | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index b98535b201..191cc94e2b 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -281,11 +281,6 @@ let get_cache opt = function | "force" -> Some Stm.AsyncOpts.Force | _ -> prerr_endline ("Error: force expected after "^opt); exit 1 -let get_identifier opt s = - try Names.Id.of_string s - with CErrors.UserError _ -> - prerr_endline ("Error: valid identifier expected after option "^opt); exit 1 - let is_not_dash_option = function | Some f when String.length f > 0 && f.[0] <> '-' -> true | _ -> false @@ -478,7 +473,9 @@ let parse_args arglist : coq_cmdopts * string list = add_load_vernacular oval true (next ()) |"-mangle-names" -> - Namegen.set_mangle_names_mode (get_identifier opt (next ())); oval + Goptions.set_bool_option_value ["Mangle"; "Names"] true; + Goptions.set_string_option_value ["Mangle"; "Names"; "Prefix"] (next ()); + oval |"-print-mod-uid" -> let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0 |