Remove obj_sec field of Nametab.obj_prefix record.

There are no more users.

5 files changed, 12 insertions, 17 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
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 03921bca30..4cc6bc2052 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -213,7 +213,7 @@ let print_kn locals kn =
 let nametab_register_dir obj_mp =
   let id = mk_fake_top () in
   let obj_dir = DirPath.make [id] in
-  Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirModule { obj_dir; obj_mp; obj_sec = DirPath.empty }))
+  Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirModule { obj_dir; obj_mp; }))
 
 (** Nota: the [global_reference] we register in the nametab below
     might differ from internal ones, since we cannot recreate here
diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml
index 58a7dff5fd..c7b68d18c2 100644
--- a/vernac/declaremods.ml
+++ b/vernac/declaremods.ml
@@ -211,7 +211,7 @@ let compute_visibility exists i =
 (** Iterate some function [iter_objects] on all components of a module *)
 
 let do_module exists iter_objects i obj_dir obj_mp sobjs kobjs =
-  let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in
+  let prefix = Nametab.{ obj_dir ; obj_mp; } in
   let dirinfo = Nametab.GlobDirRef.DirModule prefix in
   consistency_checks exists obj_dir dirinfo;
   Nametab.push_dir (compute_visibility exists i) obj_dir dirinfo;
@@ -266,14 +266,14 @@ and load_objects i prefix objs =
 and load_include i ((sp,kn), aobjs) =
   let obj_dir = Libnames.dirpath sp in
   let obj_mp = KerName.modpath kn in
-  let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in
+  let prefix = Nametab.{ obj_dir; obj_mp; } in
   let o = expand_aobjs aobjs in
   load_objects i prefix o
 
 and load_keep i ((sp,kn),kobjs) =
   (* Invariant : seg isn't empty *)
   let obj_dir = dir_of_sp sp and obj_mp  = mp_of_kn kn in
-  let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in
+  let prefix = Nametab.{ obj_dir ; obj_mp; } in
   let modobjs =
     try ModObjs.get obj_mp
     with Not_found -> assert false (* a substobjs should already be loaded *)
@@ -327,7 +327,7 @@ let rec open_object i (name, obj) =
   | KeepObject objs -> open_keep i (name, objs)
 
 and open_module i obj_dir obj_mp sobjs =
-  let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in
+  let prefix = Nametab.{ obj_dir ; obj_mp; } in
   let dirinfo = Nametab.GlobDirRef.DirModule prefix in
   consistency_checks true obj_dir dirinfo;
   Nametab.push_dir (Nametab.Exactly i) obj_dir dirinfo;
@@ -353,7 +353,7 @@ and open_modtype i ((sp,kn),_) =
 and open_include i ((sp,kn), aobjs) =
   let obj_dir = Libnames.dirpath sp in
   let obj_mp = KerName.modpath kn in
-  let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in
+  let prefix = Nametab.{ obj_dir; obj_mp; } in
   let o = expand_aobjs aobjs in
   open_objects i prefix o
 
@@ -363,7 +363,7 @@ and open_export i mpl =
 
 and open_keep i ((sp,kn),kobjs) =
   let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in
-  let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in
+  let prefix = Nametab.{ obj_dir; obj_mp; } in
   open_objects i prefix kobjs
 
 let rec cache_object (name, obj) =
@@ -380,7 +380,7 @@ let rec cache_object (name, obj) =
 and cache_include ((sp,kn), aobjs) =
   let obj_dir = Libnames.dirpath sp in
   let obj_mp = KerName.modpath kn in
-  let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in
+  let prefix = Nametab.{ obj_dir; obj_mp; } in
   let o = expand_aobjs aobjs in
   load_objects 1 prefix o;
   open_objects 1 prefix o