From b1a3ea4855b1e150b2e677a6d5466458893d6c60 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 15 May 2019 18:47:22 +0200
Subject: Inverting the responsibility to define logically a constant in
 Declare.

The code was intricate due to the special handling of side-effects, while
it was sufficient to extrude the logical definition to make it clearer. We
thus declare a constant in two parts, first purely kernel-related, then
purely libobject-related.
---
 library/lib.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'library/lib.mli')

diff --git a/library/lib.mli b/library/lib.mli
index 30569197bc..5da76961a6 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -57,7 +57,6 @@ val segment_of_objects :
 
 val add_leaf : Id.t -> Libobject.obj -> Libobject.object_name
 val add_anonymous_leaf : ?cache_first:bool -> Libobject.obj -> unit
-val pull_to_head : Libobject.object_name -> unit
 
 (** this operation adds all objects with the same name and calls [load_object]
    for each of them *)
-- 
cgit v1.2.3