diff options
Diffstat (limited to 'library/lib.ml')
| -rw-r--r-- | library/lib.ml | 11 |
1 files changed, 3 insertions, 8 deletions
diff --git a/library/lib.ml b/library/lib.ml index 5e9d2baa1d..4aee82079d 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -27,11 +27,10 @@ type node = | CompilingLibrary of object_prefix | OpenedModule of is_type * export * object_prefix * Summary.frozen | OpenedSection of object_prefix * Summary.frozen - | ClosedSection of library_segment -and library_entry = object_name * node +type library_entry = object_name * node -and library_segment = library_entry list +type library_segment = library_entry list type lib_objects = (Names.Id.t * obj) list @@ -72,7 +71,6 @@ let classify_segment seg = clean ((id,o')::substl, keepl, anticipl) stk | Anticipate o' -> clean (substl, keepl, o'::anticipl) stk) - | (_,ClosedSection _) :: stk -> clean acc stk | (_,OpenedSection _) :: _ -> user_err Pp.(str "there are still opened sections") | (_,OpenedModule (ty,_,_,_)) :: _ -> user_err ~hdr:"Lib.classify_segment" @@ -550,7 +548,6 @@ let discharge_item ((sp,_ as oname),e) = match e with | Leaf lobj -> Option.map (fun o -> (basename sp,o)) (discharge_object (oname,lobj)) - | ClosedSection _ -> None | OpenedSection _ | OpenedModule _ | CompilingLibrary _ -> anomaly (Pp.str "discharge_item.") @@ -565,7 +562,6 @@ let close_section () = let (secdecls,mark,before) = split_lib_at_opening oname in lib_state := { !lib_state with lib_stk = before }; pop_path_prefix (); - add_entry oname (ClosedSection (List.rev (mark::secdecls))); let newdecls = List.map discharge_item secdecls in Summary.unfreeze_summaries fs; List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls @@ -585,8 +581,7 @@ let freeze ~marshallable = | n, OpenedModule (it,e,op,_) -> Some(n,OpenedModule(it,e,op,Summary.empty_frozen)) | n, OpenedSection (op, _) -> - Some(n,OpenedSection(op,Summary.empty_frozen)) - | n, ClosedSection _ -> Some (n,ClosedSection [])) + Some(n,OpenedSection(op,Summary.empty_frozen))) !lib_state.lib_stk in { !lib_state with lib_stk } | _ -> |