diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-05-11 19:10:52 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-05-11 19:10:52 +0200 |
| commit | 7dd881fc72d62eb0c1f1e5063eb3a8ed268fb5d5 (patch) | |
| tree | 6504707bb85c3ea9dcae9389a9e8ec639159a753 /library/lib.ml | |
| parent | 7a6cac1942281fbd66c0e46e3be068b9198addce (diff) | |
| parent | ea24fed3a1a91f945d0cce380d0ea1a9156e735e (diff) | |
Merge PR #7340: Remove DirClosedSection.
Diffstat (limited to 'library/lib.ml')
| -rw-r--r-- | library/lib.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/library/lib.ml b/library/lib.ml index 0e4106317..8a54995b9 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -569,13 +569,11 @@ let close_section () = in let (secdecls,mark,before) = split_lib_at_opening oname in lib_state := { !lib_state with lib_stk = before }; - let full_olddir = !lib_state.path_prefix.obj_dir in 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; - Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir) + List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls (* State and initialization. *) |