diff options
Diffstat (limited to 'library/lib.ml')
| -rw-r--r-- | library/lib.ml | 30 |
1 files changed, 15 insertions, 15 deletions
diff --git a/library/lib.ml b/library/lib.ml index c3c480aee4..9cce9b92ad 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -133,7 +133,10 @@ let cwd () = !lib_state.path_prefix.Nametab.obj_dir let current_mp () = !lib_state.path_prefix.Nametab.obj_mp let current_sections () = Safe_typing.sections_of_safe_env (Global.safe_env()) -let sections_depth () = Section.depth (current_sections()) +let sections_depth () = match current_sections() with + | None -> 0 + | Some sec -> Section.depth sec + let sections_are_opened = Global.sections_are_opened let cwd_except_section () = @@ -240,15 +243,6 @@ let add_discharged_leaf id obj = cache_object (oname,newobj); add_entry oname (Leaf (AtomicObject newobj)) -let add_leaves id objs = - let oname = make_foname id in - let add_obj obj = - add_entry oname (Leaf (AtomicObject obj)); - load_object 1 (oname,obj) - in - List.iter add_obj objs; - oname - let add_anonymous_leaf ?(cache_first = true) obj = let id = anonymous_id () in let oname = make_foname id in @@ -417,14 +411,18 @@ let extract_worklist info = let sections () = Safe_typing.sections_of_safe_env @@ Global.safe_env () +let force_sections () = match Safe_typing.sections_of_safe_env (Global.safe_env()) with + | Some s -> s + | None -> CErrors.user_err Pp.(str "No open section.") + let replacement_context () = - Section.replacement_context (Global.env ()) (sections ()) + Section.replacement_context (Global.env ()) (force_sections ()) let section_segment_of_constant con = - Section.segment_of_constant (Global.env ()) con (sections ()) + Section.segment_of_constant (Global.env ()) con (force_sections ()) let section_segment_of_mutual_inductive kn = - Section.segment_of_inductive (Global.env ()) kn (sections ()) + Section.segment_of_inductive (Global.env ()) kn (force_sections ()) let empty_segment = Section.empty_segment @@ -437,8 +435,10 @@ let section_segment_of_reference = let open GlobRef in function let variable_section_segment_of_reference gr = (section_segment_of_reference gr).Section.abstr_ctx -let is_in_section ref = - Section.is_in_section (Global.env ()) ref (sections ()) +let is_in_section ref = match sections () with + | None -> false + | Some sec -> + Section.is_in_section (Global.env ()) ref sec let section_instance = let open GlobRef in function | VarRef id -> |