From eacc77c5816a00b99aaef0d5ff596a3078b0a208 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 27 Nov 2018 16:33:36 +0100
Subject: [lib] Remove leftover flag `print_mod_uid`

The whole `native_name_from_filename` business seems quite strange tho.
---
 lib/flags.ml  | 3 ---
 lib/flags.mli | 4 +---
 2 files changed, 1 insertion(+), 6 deletions(-)

(limited to 'lib')

diff --git a/lib/flags.ml b/lib/flags.ml
index 3aef5a7b2c..ae4d337ded 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -123,8 +123,5 @@ let get_inline_level () = !inline_level
 (* Native code compilation for conversion and normalization *)
 let output_native_objects = ref false
 
-(* Print the mod uid associated to a vo file by the native compiler *)
-let print_mod_uid = ref false
-
 let profile_ltac = ref false
 let profile_ltac_cutoff = ref 2.0
diff --git a/lib/flags.mli b/lib/flags.mli
index e282d4ca8c..d883cf1e30 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -119,8 +119,6 @@ val default_inline_level : int
 (** When producing vo objects, also compile the native-code version *)
 val output_native_objects : bool ref
 
-(** Print the mod uid associated to a vo file by the native compiler *)
-val print_mod_uid : bool ref
-
+(** Global profile_ltac flag  *)
 val profile_ltac : bool ref
 val profile_ltac_cutoff : float ref
-- 
cgit v1.2.3