From afd214869f050d07f9774d770c289bdc6e602dfd Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sun, 13 Oct 2019 16:35:47 +0200
Subject: Remove obj_sec field of Nametab.obj_prefix record.

There are no more users.
---
 printing/printmod.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'printing')

diff --git a/printing/printmod.ml b/printing/printmod.ml
index 03921bca30..4cc6bc2052 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -213,7 +213,7 @@ let print_kn locals kn =
 let nametab_register_dir obj_mp =
   let id = mk_fake_top () in
   let obj_dir = DirPath.make [id] in
-  Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirModule { obj_dir; obj_mp; obj_sec = DirPath.empty }))
+  Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirModule { obj_dir; obj_mp; }))
 
 (** Nota: the [global_reference] we register in the nametab below
     might differ from internal ones, since we cannot recreate here
-- 
cgit v1.2.3