From 181597904ae9211facaa406371b5d54d61f40cbf Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 4 Jul 2019 10:16:26 +0200
Subject: Remove library-specific code for `Import`.

Libraries are now handled like other modules.
---
 checker/check.ml  | 1 -
 checker/values.ml | 2 +-
 2 files changed, 1 insertion(+), 2 deletions(-)

(limited to 'checker')

diff --git a/checker/check.ml b/checker/check.ml
index ecf84fda9c..69de2536c5 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -262,7 +262,6 @@ let raw_intern_library f =
 
 type summary_disk = {
   md_name : compilation_unit_name;
-  md_imports : compilation_unit_name array;
   md_deps : (compilation_unit_name * Safe_typing.vodigest) array;
 }
 
diff --git a/checker/values.ml b/checker/values.ml
index cc9ac1f834..708419e7cc 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -395,7 +395,7 @@ let v_stm_seg = v_pair v_tasks v_counters
 (** Toplevel structures in a vo (see Cic.mli) *)
 
 let v_libsum =
-  Tuple ("summary", [|v_dp;Array v_dp;v_deps|])
+  Tuple ("summary", [|v_dp;v_deps|])
 
 let v_lib =
   Tuple ("library",[|v_compiled_lib;v_libraryobjs|])
-- 
cgit v1.2.3


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

(limited to 'checker')

diff --git a/checker/values.ml b/checker/values.ml
index 708419e7cc..1590097731 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -357,7 +357,7 @@ and v_libobjt = Sum("Libobject.t",0,
      [| v_substobjs |];
      [| v_aobjs |];
      [| v_libobjs |];
-     [| v_bool; v_mp |];
+     [| v_mp |];
      [| v_obj |]
   |])
 
-- 
cgit v1.2.3


From 24fc879cf2380bb28dd8c0f5ff8c7805ad121e1f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 12 Sep 2019 20:49:48 +0200
Subject: Optimize multiple imports

---
 checker/values.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'checker')

diff --git a/checker/values.ml b/checker/values.ml
index 1590097731..6b340635d7 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -357,7 +357,7 @@ and v_libobjt = Sum("Libobject.t",0,
      [| v_substobjs |];
      [| v_aobjs |];
      [| v_libobjs |];
-     [| v_mp |];
+     [| List v_mp |];
      [| v_obj |]
   |])
 
-- 
cgit v1.2.3