aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqargs.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-08 10:37:10 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-08 10:37:10 +0100
commit563199757c5756fb5858da1b684162566a73fa3e (patch)
tree0c320308919b973a82c1c6ca68edbf0e6c4054e4 /toplevel/coqargs.ml
parent7aaab2936e94eed9bc56eeb8430e0821158af86a (diff)
parent5968648f9e9db09de462dd8c3530febd66466312 (diff)
Merge PR #6582: Mangle auto-generated names
Diffstat (limited to 'toplevel/coqargs.ml')
-rw-r--r--toplevel/coqargs.ml8
1 files changed, 8 insertions, 0 deletions
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 06b2ba41b..a1a07fce8 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -271,6 +271,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
@@ -466,6 +471,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