diff options
| author | Maxime Dénès | 2018-07-19 23:58:52 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-07-20 18:43:37 +0200 |
| commit | 32caa7b700cb2f561edec9b86fbb4583d2962d4d (patch) | |
| tree | 96071b71c12b72b0932c044f5bc2a4eb28f536de /library/lib.mli | |
| parent | 6a9d0dc7b5c9a6a1c10c0c94eba5e72543080399 (diff) | |
Also remove ClosedSection (same reasoning as ClosedModule)
Diffstat (limited to 'library/lib.mli')
| -rw-r--r-- | library/lib.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/library/lib.mli b/library/lib.mli index 2915a5fd64..eff72ea63f 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -24,9 +24,8 @@ type node = | CompilingLibrary of Libnames.object_prefix | OpenedModule of is_type * export * Libnames.object_prefix * Summary.frozen | OpenedSection of Libnames.object_prefix * Summary.frozen - | ClosedSection of library_segment -and library_segment = (Libnames.object_name * node) list +type library_segment = (Libnames.object_name * node) list type lib_objects = (Id.t * Libobject.obj) list |