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 /library/lib.ml | |
| parent | c3479eceb8e07b37570a80bca9937e3520c61024 (diff) | |
Remove obj_sec field of Nametab.obj_prefix record.
There are no more users.
Diffstat (limited to 'library/lib.ml')
| -rw-r--r-- | library/lib.ml | 10 |
1 files changed, 4 insertions, 6 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 |