diff options
| author | Gaëtan Gilbert | 2019-10-13 16:35:47 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-14 10:24:26 +0200 |
| commit | afd214869f050d07f9774d770c289bdc6e602dfd (patch) | |
| tree | 7b5518a714466c675e6ca152bdb78e865510a369 /vernac | |
| parent | c3479eceb8e07b37570a80bca9937e3520c61024 (diff) | |
Remove obj_sec field of Nametab.obj_prefix record.
There are no more users.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/declaremods.ml | 14 |
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 |
