aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
authorEnrico Tassi2019-09-17 10:29:48 +0200
committerEnrico Tassi2019-09-17 10:29:48 +0200
commitc18f04422cb0827994e8d7aecc384a2c448a61c9 (patch)
tree341c0e48158cd4a732751c6aed00c9c864dbff52 /printing
parent3d7de72f45ae2f8bcedbe1db0eb8870e58757b45 (diff)
parent73b9794cc21e9fe932d5be9836fe1c53659ba717 (diff)
Merge PR #10476: Remove library-specific code for `Import`.
Reviewed-by: gares Reviewed-by: ppedrot
Diffstat (limited to 'printing')
-rw-r--r--printing/printmod.ml2
1 files changed, 1 insertions, 1 deletions
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;