From 4614010ceddb9ed5100fa4e43d2807b172143a19 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 8 Jul 2019 15:00:36 +0200
Subject: Specialize `ImportObject` to `Export`

`Import` does not actually need to register an object, only `Export`
does. So we specialize and rename the object into `ExportObject`.
---
 printing/printmod.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'printing/printmod.ml')

diff --git a/printing/printmod.ml b/printing/printmod.ml
index 43992ec9d3..141469ff9c 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -242,7 +242,7 @@ let nametab_register_body mp dir (l,body) =
 
 let nametab_register_module_body mp struc =
   (* If [mp] is a globally visible module, we simply import it *)
-  try Declaremods.really_import_module mp
+  try Declaremods.import_module ~export:false mp
   with Not_found ->
     (* Otherwise we try to emulate an import by playing with nametab *)
     nametab_register_dir mp;
-- 
cgit v1.2.3