From ea24fed3a1a91f945d0cce380d0ea1a9156e735e Mon Sep 17 00:00:00 2001
From: Jasper Hugunin <jasperh@cs.washington.edu>
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 +---
 library/libnames.ml  | 3 ---
 library/libnames.mli | 2 --
 library/nametab.ml   | 1 -
 printing/prettyp.ml  | 1 -
 5 files changed, 1 insertion(+), 10 deletions(-)

diff --git a/library/lib.ml b/library/lib.ml
index 543cb45bc..fde13d0e3 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. *)
 
diff --git a/library/libnames.ml b/library/libnames.ml
index d84731322..4ceea480d 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -174,8 +174,6 @@ type global_dir_reference =
   | DirOpenModtype of object_prefix
   | DirOpenSection of object_prefix
   | DirModule of object_prefix
-  | DirClosedSection of DirPath.t
-      (* this won't last long I hope! *)
 
 let eq_op op1 op2 =
   DirPath.equal op1.obj_dir op2.obj_dir &&
@@ -187,7 +185,6 @@ let eq_global_dir_reference r1 r2 = match r1, r2 with
 | DirOpenModtype op1, DirOpenModtype op2 -> eq_op op1 op2
 | DirOpenSection op1, DirOpenSection op2 -> eq_op op1 op2
 | DirModule op1, DirModule op2 -> eq_op op1 op2
-| DirClosedSection dp1, DirClosedSection dp2 -> DirPath.equal dp1 dp2
 | _ -> false
 
 type reference_r =
diff --git a/library/libnames.mli b/library/libnames.mli
index 9dad26129..81e5bc5b1 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -125,8 +125,6 @@ type global_dir_reference =
   | DirOpenModtype of object_prefix
   | DirOpenSection of object_prefix
   | DirModule of object_prefix
-  | DirClosedSection of DirPath.t
-      (** this won't last long I hope! *)
 
 val eq_global_dir_reference : 
   global_dir_reference -> global_dir_reference -> bool
diff --git a/library/nametab.ml b/library/nametab.ml
index 2046bf758..995f44706 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -432,7 +432,6 @@ let full_name_module qid =
 let locate_section qid =
   match locate_dir qid with
     | DirOpenSection { obj_dir; _ } -> obj_dir
-    | DirClosedSection dir -> dir
     | _ -> raise Not_found
 
 let locate_all qid =
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 1f17d844f..9c7408596 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -376,7 +376,6 @@ let pr_located_qualid = function
         | DirOpenModtype { obj_dir ; _ } -> "Open Module Type", obj_dir
         | DirOpenSection { obj_dir ; _ } -> "Open Section", obj_dir
         | DirModule { obj_dir ; _ } -> "Module", obj_dir
-	| DirClosedSection dir -> "Closed Section", dir
       in
       str s ++ spc () ++ DirPath.print dir
   | ModuleType mp ->
-- 
cgit v1.2.3