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

(limited to 'library/library.ml')

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