From c408e819ce39b27f0842c84b1b24c585ac5b6086 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 22 Mar 2017 01:14:50 +0100
Subject: [lib] [api] Introduce record for `object_prefix`

This is a minor cleanup adding a record in a try to structure the
state living in `Lib`.
---
 vernac/vernacentries.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index bdd351901d..c5653ceb74 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -185,8 +185,8 @@ let print_module r =
   try
     let globdir = Nametab.locate_dir qid in
       match globdir with
-	  DirModule (dirpath,(mp,_)) ->
-	    Feedback.msg_notice (Printmod.print_module (Printmod.printable_body dirpath) mp)
+          DirModule { obj_dir; obj_mp; _ } ->
+            Feedback.msg_notice (Printmod.print_module (Printmod.printable_body obj_dir) obj_mp)
 	| _ -> raise Not_found
   with
       Not_found -> Feedback.msg_error (str"Unknown Module " ++ pr_qualid qid)
-- 
cgit v1.2.3