diff options
| author |  Jasper Hugunin <jasperh@cs.washington.edu> | 2018-02-17 07:35:57 -0800 |
|---|---|---|
| committer | Jasper Hugunin <jasperh@cs.washington.edu> | 2018-02-17 07:35:57 -0800 |
| commit | 5968648f9e9db09de462dd8c3530febd66466312 (patch) | |
| tree | 32b40e69b44345209042481fef71c26a4525f778 /toplevel | |
| parent | 8dd6d091ffbfa237f7266eeca60187263a9b521f (diff) | |
Implement name mangling option
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqargs.ml | 8 | ||||
| -rw-r--r-- | toplevel/usage.ml | 1 |
2 files changed, 9 insertions, 0 deletions
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 5b73471c5..1fdcd2bd4 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -270,6 +270,11 @@ 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 @@ -465,6 +470,9 @@ let parse_args arglist : coq_cmdopts * string list = |"-load-vernac-source-verbose"|"-lv" -> add_load_vernacular oval true (next ()) + |"-mangle-names" -> + Namegen.set_mangle_names_mode (get_identifier opt (next ())); oval + |"-print-mod-uid" -> let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0 diff --git a/toplevel/usage.ml b/toplevel/usage.ml index f0215b678..e28637f2e 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -77,6 +77,7 @@ let print_usage_channel co command = \n -impredicative-set set sort Set impredicative\ \n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\ \n -type-in-type disable universe consistency checking\ +\n -mangle-names x mangle auto-generated names using prefix x\ \n -time display the time taken by each command\ \n -profile-ltac display the time taken by each (sub)tactic\ \n -m, --memory display total heap size at program exit\ |