From 0adc2073cf3e7bd3b2d9ee2cdf75e16e3a243c44 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 31 Oct 2018 09:39:53 +0100
Subject: [nametab] Move global_dir_reference to Nametab

This type is "private" to the Nametab, which manages it. It thus makes
sense IMHO to live there.
---
 library/lib.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library/lib.ml')

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 ()
 
-- 
cgit v1.2.3