From bb2e6a2ceea202ef0bfff2b3a0ddf22491d75f26 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 13 Oct 2019 17:09:37 +0200
Subject: Remove the unused add_leaves Libobject primitive.

---
 library/lib.ml | 9 ---------
 1 file changed, 9 deletions(-)

(limited to 'library/lib.ml')

diff --git a/library/lib.ml b/library/lib.ml
index 6c47d6c6ae..9cce9b92ad 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -243,15 +243,6 @@ let add_discharged_leaf id obj =
   cache_object (oname,newobj);
   add_entry oname (Leaf (AtomicObject newobj))
 
-let add_leaves id objs =
-  let oname = make_foname id in
-  let add_obj obj =
-    add_entry oname (Leaf (AtomicObject obj));
-    load_object 1 (oname,obj)
-  in
-  List.iter add_obj objs;
-  oname
-
 let add_anonymous_leaf ?(cache_first = true) obj =
   let id = anonymous_id () in
   let oname = make_foname id in
-- 
cgit v1.2.3