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, 11 insertions, 0 deletions

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index e597ea9a9..b0f320942 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -211,6 +211,17 @@ let join_constant_body cb =
   | OpaqueDef d -> ignore(Future.join d)
   | _ -> ()
 
+let prune_constant_body cb =
+  let cst, cbo = cb.const_constraints, cb.const_body in
+  let cst' = Future.drop cst in
+  let cbo' = match cbo with
+    | OpaqueDef d ->
+        let d' = Future.drop d in
+        if d' == d then cbo else OpaqueDef d'
+    | _ -> cbo in
+  if cst' == cst && cbo' == cbo then cb
+  else {cb with const_constraints = cst'; const_body = cbo'}
+
 let string_of_side_effect = function
   | NewConstant (c,_) -> Names.string_of_con c
 type side_effects = side_effect list