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.
---
 vernac/vernacentries.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 1190d73258..088ba6552b 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -185,6 +185,7 @@ let print_modules () =
 
 let print_module qid =
   try
+    let open Nametab.GlobDirRef in
     let globdir = Nametab.locate_dir qid in
       match globdir with
           DirModule { obj_dir; obj_mp; _ } ->
-- 
cgit v1.2.3