diff options
author | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-12 16:32:06 +0000 |
---|---|---|
committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-12 16:32:06 +0000 |
commit | 774159f7805bfddeb253e39bcd8271c58038ca39 (patch) | |
tree | 608734369024d43639c7733ba3afe35407285562 /library | |
parent | 3e8db9f159e534dd194817550f8b5664febc4477 (diff) |
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
Diffstat (limited to 'library')
-rw-r--r-- | library/lib.ml | 10 |
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; |