From 1a8a8db7a9e4eb5ab56cd192411529661a4972c7 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Wed, 23 Dec 2015 14:27:13 +0100
Subject: Remove Library.mem, which is pointless since 8.5.

---
 library/library.ml  | 7 -------
 library/library.mli | 3 ---
 2 files changed, 10 deletions(-)

diff --git a/library/library.ml b/library/library.ml
index 7aaa8b2e6..db95213fe 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -769,13 +769,6 @@ let save_library_raw f sum lib univs proofs =
   System.marshal_out_segment f' ch (proofs     : seg_proofs);
   close_out ch
 
-(************************************************************************)
-(*s Display the memory use of a library. *)
-
-open Printf
-
-let mem s = Pp.mt ()
-
 module StringOrd = struct type t = string let compare = String.compare end
 module StringSet = Set.Make(StringOrd)
 
diff --git a/library/library.mli b/library/library.mli
index d5e610dd6..71aefdbd8 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -82,8 +82,5 @@ val locate_qualified_library :
 
 *)
 
-(** {6 Statistics: display the memory use of a library. } *)
-val mem : DirPath.t -> Pp.std_ppcmds
-
 (** {6 Native compiler. } *)
 val native_name_from_filename : string -> string
-- 
cgit v1.2.3