Remove obj_sec field of Nametab.obj_prefix record.

There are no more users.

3 files changed, 4 insertions, 9 deletions

diff --git a/library/lib.ml b/library/lib.ml
index 3f162682c3..80b50b26d0 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -107,7 +107,6 @@ let segment_of_objects prefix =
 let initial_prefix = Nametab.{
   obj_dir = default_library;
   obj_mp  = ModPath.initial;
-  obj_sec = DirPath.empty;
 }
 
 type lib_state = {
@@ -169,7 +168,6 @@ let pop_path_prefix () =
   let op = !lib_state.path_prefix in
   lib_state := { !lib_state
                  with path_prefix = Nametab.{ op with obj_dir = pop_dirpath op.obj_dir;
-                                                      obj_sec = pop_dirpath op.obj_sec;
                                             } }
 
 let find_entry_p p =
@@ -282,7 +280,7 @@ let current_mod_id () =
 
 let start_mod is_type export id mp fs =
   let dir = add_dirpath_suffix (!lib_state.path_prefix.Nametab.obj_dir) id in
-  let prefix = Nametab.{ obj_dir = dir; obj_mp = mp; obj_sec = Names.DirPath.empty } in
+  let prefix = Nametab.{ obj_dir = dir; obj_mp = mp; } in
   let exists =
     if is_type then Nametab.exists_cci (make_path id)
     else Nametab.exists_dir dir
@@ -330,9 +328,9 @@ let contents_after sp = let (after,_,_) = split_lib sp in after
 let start_compilation s mp =
   if !lib_state.comp_name != None then
     user_err Pp.(str "compilation unit is already started");
-  if not (Names.DirPath.is_empty (!lib_state.path_prefix.Nametab.obj_sec)) then
+  if Global.sections_are_opened () then (* XXX not sure if we need this check *)
     user_err Pp.(str "some sections are already opened");
-  let prefix = Nametab.{ obj_dir = s; obj_mp = mp; obj_sec = DirPath.empty } in
+  let prefix = Nametab.{ obj_dir = s; obj_mp = mp } in
   add_anonymous_entry (CompilingLibrary prefix);
   lib_state := { !lib_state with comp_name = Some s;
                                  path_prefix = prefix }
@@ -465,7 +463,7 @@ let open_section id =
   let () = Global.open_section () in
   let opp = !lib_state.path_prefix in
   let obj_dir = add_dirpath_suffix opp.Nametab.obj_dir id in
-  let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in
+  let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; } in
   if Nametab.exists_dir obj_dir then
     user_err ~hdr:"open_section" (Id.print id ++ str " already exists.");
   let fs = Summary.freeze_summaries ~marshallable:false in
diff --git a/library/nametab.ml b/library/nametab.ml
index aed7d08ac1..8626ee1c59 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -18,12 +18,10 @@ open Globnames
 type object_prefix = {
   obj_dir : DirPath.t;
   obj_mp  : ModPath.t;
-  obj_sec : DirPath.t;
 }
 
 let eq_op op1 op2 =
   DirPath.equal op1.obj_dir op2.obj_dir &&
-  DirPath.equal op1.obj_sec op2.obj_sec &&
   ModPath.equal op1.obj_mp  op2.obj_mp
 
 (* to this type are mapped DirPath.t's in the nametab *)
diff --git a/library/nametab.mli b/library/nametab.mli
index 6ee22fc283..55458fe2c6 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -74,7 +74,6 @@ open Globnames
 type object_prefix = {
   obj_dir : DirPath.t;
   obj_mp  : ModPath.t;
-  obj_sec : DirPath.t;
 }
 
 val eq_op : object_prefix -> object_prefix -> bool