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

(limited to 'library/lib.mli')

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