From 80aba8d52c650ef8e4ada694c20bf12c15849694 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Thu, 8 Aug 2013 18:52:47 +0000
Subject: 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
---
 kernel/declareops.ml | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'kernel/declareops.ml')

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index e597ea9a91..b0f320942e 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
-- 
cgit v1.2.3