From f5ec3f5cbd4bc2e0f65e1c52143b199ce7c2a5ad Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 6 Jan 2021 17:13:59 +0100
Subject: [coqtop] handle -print-module-uid after initialization

---
 sysinit/coqargs.ml | 12 ------------
 1 file changed, 12 deletions(-)

(limited to 'sysinit')

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 ());
-- 
cgit v1.2.3