diff options
Diffstat (limited to 'library/lib.ml')
| -rw-r--r-- | library/lib.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/lib.ml b/library/lib.ml index 1acc8fd8fd..762a2e0567 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -551,7 +551,7 @@ let open_section id = let fs = Summary.freeze_summaries ~marshallable:`No in add_entry (make_oname id) (OpenedSection (prefix, fs)); (*Pushed for the lifetime of the section: removed by unfrozing the summary*) - Nametab.push_dir (Nametab.Until 1) obj_dir (DirOpenSection prefix); + Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirOpenSection prefix)); lib_state := { !lib_state with path_prefix = prefix }; add_section () |