diff options
Diffstat (limited to 'library/lib.ml')
| -rw-r--r-- | library/lib.ml | 30 |
1 files changed, 11 insertions, 19 deletions
diff --git a/library/lib.ml b/library/lib.ml index 0d9efe2d5d..630c860a61 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 = { @@ -132,10 +131,10 @@ let library_dp () = let cwd () = !lib_state.path_prefix.Nametab.obj_dir let current_mp () = !lib_state.path_prefix.Nametab.obj_mp -let current_sections () = !lib_state.path_prefix.Nametab.obj_sec +let current_sections () = Safe_typing.sections_of_safe_env (Global.safe_env()) -let sections_depth () = List.length (Names.DirPath.repr (current_sections ())) -let sections_are_opened () = not (Names.DirPath.is_empty (current_sections ())) +let sections_depth () = Section.depth (current_sections()) +let sections_are_opened = Global.sections_are_opened let cwd_except_section () = Libnames.pop_dirpath_n (sections_depth ()) (cwd ()) @@ -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 } @@ -410,18 +408,12 @@ let find_opening_node id = - the list of substitution to do at section closing *) -type abstr_info = Section.abstr_info = private { - abstr_ctx : Constr.named_context; - abstr_subst : Univ.Instance.t; - abstr_uctx : Univ.AUContext.t; -} - let instance_from_variable_context = List.rev %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list let extract_worklist info = - let args = instance_from_variable_context info.abstr_ctx in - info.abstr_subst, args + let args = instance_from_variable_context info.Section.abstr_ctx in + info.Section.abstr_subst, args let sections () = Safe_typing.sections_of_safe_env @@ Global.safe_env () @@ -443,7 +435,7 @@ let section_segment_of_reference = let open GlobRef in function | VarRef _ -> empty_segment let variable_section_segment_of_reference gr = - (section_segment_of_reference gr).abstr_ctx + (section_segment_of_reference gr).Section.abstr_ctx let is_in_section ref = Section.is_in_section (Global.env ()) ref (sections ()) @@ -465,7 +457,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 @@ -559,7 +551,7 @@ let discharge_proj_repr = let _, newpars = Mindmap.find mind (snd modlist) in mind, npars + Array.length newpars) -let discharge_abstract_universe_context { abstr_subst = subst; abstr_uctx = abs_ctx } auctx = +let discharge_abstract_universe_context { Section.abstr_subst = subst; abstr_uctx = abs_ctx } auctx = let open Univ in let ainst = make_abstract_instance auctx in let subst = Instance.append subst ainst in |