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 --- library/declaremods.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'library/declaremods.ml') diff --git a/library/declaremods.ml b/library/declaremods.ml index c8f9d6161..0dfee9787 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -822,7 +822,7 @@ end (** {6 Module operations handling summary freeze/unfreeze *) let protect_summaries f = - let fs = Summary.freeze_summaries ~marshallable:false in + let fs = Summary.freeze_summaries ~marshallable:`No in try f fs with reraise -> (* Something wrong: undo the whole process *) -- cgit v1.2.3