From 813c4f65e80926cb4f1eadf1a6eeda6983b71a2b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 31 Oct 2018 09:55:57 +0100
Subject: [nametab] Move `object_prefix` to `Nametab`.

We move `object_prefix` to `Nametab`. This highlights the coupling of
`Lib` and `Nametab` wrt naming.

This also thins `Libname`, which IMHO is a good thing as we are
talking about "local, internal" naming here.
---
 vernac/vernacentries.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 088ba6552b..787134c173 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -188,7 +188,7 @@ let print_module qid =
     let open Nametab.GlobDirRef in
     let globdir = Nametab.locate_dir qid in
       match globdir with
-          DirModule { obj_dir; obj_mp; _ } ->
+          DirModule Nametab.{ obj_dir; obj_mp; _ } ->
           Printmod.print_module (Printmod.printable_body obj_dir) obj_mp
 	| _ -> raise Not_found
   with
-- 
cgit v1.2.3