From ea24fed3a1a91f945d0cce380d0ea1a9156e735e Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Tue, 24 Apr 2018 21:36:59 -0700
Subject: Remove DirClosedSection.

This has been around for at least 16 years, with the comment
"this won't last long I hope".
https://github.com/coq/coq/commit/12965209478bd99dfbe57f07d5b525e51b903f22#diff-1a3a6f7bd5b2cf1bc6dd43ee04bbc3eaR112
---
 library/lib.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'library/lib.ml')

diff --git a/library/lib.ml b/library/lib.ml
index 543cb45bc2..fde13d0e30 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -580,13 +580,11 @@ let close_section () =
   in
   let (secdecls,mark,before) = split_lib_at_opening oname in
   lib_state := { !lib_state with lib_stk = before };
-  let full_olddir = !lib_state.path_prefix.obj_dir in
   pop_path_prefix ();
   add_entry oname (ClosedSection (List.rev (mark::secdecls)));
   let newdecls = List.map discharge_item secdecls in
   Summary.unfreeze_summaries fs;
-  List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls;
-  Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir)
+  List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls
 
 (* State and initialization. *)
 
-- 
cgit v1.2.3