Remove the unused add_leaves Libobject primitive.

2 files changed, 0 insertions, 13 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
diff --git a/library/lib.mli b/library/lib.mli
index a313a62c2e..0d03046dc2 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -65,10 +65,6 @@ val add_anonymous_entry : node -> unit
 val add_leaf : Id.t -> Libobject.obj -> Libobject.object_name
 val add_anonymous_leaf : ?cache_first:bool -> Libobject.obj -> unit
 
-(** this operation adds all objects with the same name and calls [load_object]
-   for each of them *)
-val add_leaves : Id.t -> Libobject.obj list -> Libobject.object_name
-
 (** {6 ... } *)
 
 (** The function [contents] gives access to the current entire segment *)