enhance marshallable option for freeze (minor TODO in safe_typing)

It can be:
`Yes      Full data, in a state that can be marshalled
`No       Full data, good for Undo only
`Shallow  Partial data, marshallable, good for slave processes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16682 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 3 deletions

diff --git a/library/lib.ml b/library/lib.ml
index b4371812b..379d0e8ad 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -250,7 +250,7 @@ let add_anonymous_leaf obj =
 
 let add_frozen_state () =
   add_anonymous_entry
-    (FrozenState (Summary.freeze_summaries ~marshallable:false))
+    (FrozenState (Summary.freeze_summaries ~marshallable:`No))
 
 (* Modules. *)
 
@@ -485,7 +485,7 @@ let open_section id =
   let name = make_path id, make_kn id (* this makes little sense however *) in
   if Nametab.exists_section dir then
     errorlabstrm "open_section" (pr_id id ++ str " already exists.");
-  let fs = Summary.freeze_summaries ~marshallable:false in
+  let fs = Summary.freeze_summaries ~marshallable:`No in
   add_entry name (OpenedSection (prefix, fs));
   (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
   Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix);
@@ -529,7 +529,9 @@ let close_section () =
 
 type frozen = Names.DirPath.t option * library_segment
 
-let freeze ~marshallable:_ = (!comp_name, !lib_stk)
+let freeze ~marshallable =
+  if marshallable = `Shallow then !comp_name, []
+  else !comp_name, !lib_stk
 
 let unfreeze (mn,stk) =
   comp_name := mn;