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

1 files changed, 8 insertions, 2 deletions

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;