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

(limited to 'library/lib.ml')

diff --git a/library/lib.ml b/library/lib.ml
index a046360822..4be288ed20 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -211,9 +211,6 @@ let split_lib_at_opening sp =
 let add_entry sp node =
   lib_state := { !lib_state with lib_stk = (sp,node) :: !lib_state.lib_stk }
 
-let pull_to_head oname =
-  lib_state := { !lib_state with lib_stk = (oname,List.assoc oname !lib_state.lib_stk) :: List.remove_assoc oname !lib_state.lib_stk }
-
 let anonymous_id =
   let n = ref 0 in
   fun () -> incr n; Names.Id.of_string ("_" ^ (string_of_int !n))
-- 
cgit v1.2.3