[coqtop] handle -print-module-uid after initialization

1 files changed, 0 insertions, 12 deletions

diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml
index bb0c4882e6..19350b7e98 100644
--- a/sysinit/coqargs.ml
+++ b/sysinit/coqargs.ml
@@ -220,15 +220,6 @@ let get_float ~opt n =
   with Failure _ ->
     error_wrong_arg ("Error: float expected after option "^opt)
 
-let get_native_name s =
-  (* We ignore even critical errors because this mode has to be super silent *)
-  try
-    Filename.(List.fold_left concat (dirname s)
-                [ !Nativelib.output_dir
-                ; Library.native_name_from_filename s
-                ])
-  with _ -> ""
-
 let interp_set_option opt v old =
   let open Goptions in
   let opt = String.concat " " opt in
@@ -361,9 +352,6 @@ let parse_args ~usage ~init arglist : t * string list =
       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
-
     |"-profile-ltac-cutoff" ->
       Flags.profile_ltac := true;
       Flags.profile_ltac_cutoff := get_float ~opt (next ());