From e2e88741120332f9e97459852d7361e2d8939881 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 17 Mar 2015 10:21:41 +0100
Subject: Splitting the library representation on disk in two.

The first part only contains the summary of the library, while the second
one contains the effective content of it.
---
 checker/cic.mli | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'checker/cic.mli')

diff --git a/checker/cic.mli b/checker/cic.mli
index 90a0e9feb..e875e40f0 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -417,12 +417,16 @@ type compiled_library = {
 
 type library_objects
 
-type library_disk = {
+type summary_disk = {
   md_name : compilation_unit_name;
+  md_imports : compilation_unit_name array;
+  md_deps : library_deps;
+}
+
+type library_disk = {
   md_compiled : compiled_library;
   md_objects : library_objects;
-  md_deps : library_deps;
-  md_imports : compilation_unit_name array }
+}
 
 type opaque_table = constr Future.computation array
 type univ_table =
-- 
cgit v1.2.3