Remove the unused add_leaves Libobject primitive.

1 files changed, 0 insertions, 9 deletions

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