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.mli | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'library/library.mli')

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