From 774159f7805bfddeb253e39bcd8271c58038ca39 Mon Sep 17 00:00:00 2001
From: gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 12 Sep 2013 16:32:06 +0000
Subject: Minimal implementation of `Shallow marshalling of Lib

Just sufficient to make abstract work in such an (empty) lib.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16772 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/lib.ml | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'library/lib.ml')

diff --git a/library/lib.ml b/library/lib.ml
index e8b56de70..e1dd9ae39 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -513,8 +513,14 @@ let close_section () =
 type frozen = Names.DirPath.t option * library_segment
 
 let freeze ~marshallable =
-  if marshallable = `Shallow then !comp_name, []
-  else !comp_name, !lib_stk
+  if marshallable = `Shallow then
+    (* TASSI: we should do something more sensible here *)
+    let _, initial_prefix =
+      CList.split_when (function _, CompilingLibrary _ -> true | _ -> false)
+      !lib_stk in
+    !comp_name, initial_prefix
+  else
+    !comp_name, !lib_stk
 
 let unfreeze (mn,stk) =
   comp_name := mn;
-- 
cgit v1.2.3