aboutsummaryrefslogtreecommitdiff
path: root/library/libobject.mli
diff options
context:
space:
mode:
Diffstat (limited to 'library/libobject.mli')
-rw-r--r--library/libobject.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/library/libobject.mli b/library/libobject.mli
index 3b37db4a6f..88d292ad03 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -112,7 +112,7 @@ and t =
| ModuleTypeObject of substitutive_objects
| IncludeObject of algebraic_objects
| KeepObject of objects
- | ImportObject of { export : bool; mp : Names.ModPath.t }
+ | ExportObject of { mp : Names.ModPath.t }
| AtomicObject of obj
and objects = (Names.Id.t * t) list