aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-10-13 16:35:47 +0200
committerGaëtan Gilbert2019-10-14 10:24:26 +0200
commitafd214869f050d07f9774d770c289bdc6e602dfd (patch)
tree7b5518a714466c675e6ca152bdb78e865510a369 /vernac
parentc3479eceb8e07b37570a80bca9937e3520c61024 (diff)
Remove obj_sec field of Nametab.obj_prefix record.
There are no more users.
Diffstat (limited to 'vernac')
-rw-r--r--vernac/declaremods.ml14
1 files changed, 7 insertions, 7 deletions
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