diff options
Diffstat (limited to 'library/lib.ml')
| -rw-r--r-- | library/lib.ml | 35 |
1 files changed, 16 insertions, 19 deletions
diff --git a/library/lib.ml b/library/lib.ml index 9c13cdafdb..d4381a6923 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -481,8 +481,8 @@ let named_of_variable_context = List.map fst let name_instance inst = - (** FIXME: this should probably be done at an upper level, by storing the - name information in the section data structure. *) + (* FIXME: this should probably be done at an upper level, by storing the + name information in the section data structure. *) let map lvl = match Univ.Level.name lvl with | None -> (* Having Prop/Set/Var as section universes makes no sense *) assert false @@ -491,8 +491,8 @@ let name_instance inst = let qid = Nametab.shortest_qualid_of_universe na in Name (Libnames.qualid_basename qid) with Not_found -> - (** Best-effort naming from the string representation of the level. - See univNames.ml for a similar hack. *) + (* Best-effort naming from the string representation of the level. + See univNames.ml for a similar hack. *) Name (Id.of_string_soft (Univ.Level.to_string lvl)) in Array.map map (Univ.Instance.to_array inst) @@ -571,7 +571,7 @@ let open_section id = let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in if Nametab.exists_section obj_dir then user_err ~hdr:"open_section" (Id.print id ++ str " already exists."); - let fs = Summary.freeze_summaries ~marshallable:`No in + let fs = Summary.freeze_summaries ~marshallable:false in add_entry (make_foname id) (OpenedSection (prefix, fs)); (*Pushed for the lifetime of the section: removed by unfrozing the summary*) Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirOpenSection prefix)); @@ -608,24 +608,21 @@ let close_section () = type frozen = lib_state -let freeze ~marshallable = - match marshallable with - | `Shallow -> - (* TASSI: we should do something more sensible here *) - let lib_stk = - CList.map_filter (function +let freeze ~marshallable = !lib_state + +let unfreeze st = lib_state := st + +let drop_objects st = + let lib_stk = + CList.map_filter (function | _, Leaf _ -> None | n, (CompilingLibrary _ as x) -> Some (n,x) | n, OpenedModule (it,e,op,_) -> - Some(n,OpenedModule(it,e,op,Summary.empty_frozen)) + Some(n,OpenedModule(it,e,op,Summary.empty_frozen)) | n, OpenedSection (op, _) -> - Some(n,OpenedSection(op,Summary.empty_frozen))) - !lib_state.lib_stk in - { !lib_state with lib_stk } - | _ -> - !lib_state - -let unfreeze st = lib_state := st + Some(n,OpenedSection(op,Summary.empty_frozen))) + st.lib_stk in + { st with lib_stk } let init () = unfreeze initial_lib_state; |