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`.
---
 library/libobject.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library/libobject.ml')

diff --git a/library/libobject.ml b/library/libobject.ml
index 27e7810e6c..3d4a33c74e 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -75,7 +75,7 @@ and t =
   | ModuleTypeObject of substitutive_objects
   | IncludeObject of algebraic_objects
   | KeepObject of objects
-  | ImportObject of { export : bool; mp : ModPath.t }
+  | ExportObject of { mp : ModPath.t }
   | AtomicObject of obj
 
 and objects = (Names.Id.t * t) list
-- 
cgit v1.2.3