From 24ca86389b32e42199db8faadd41918e162b8d46 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Sat, 4 Jan 2014 10:32:22 +0100
Subject: STM: modules do not prevent proofs from being ASync

---
 library/lib.ml      | 15 ++++++++++++---
 library/summary.mli |  1 +
 2 files changed, 13 insertions(+), 3 deletions(-)

(limited to 'library')

diff --git a/library/lib.ml b/library/lib.ml
index 6bbf8ef47..eef8171cc 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -516,10 +516,19 @@ let freeze ~marshallable =
   match marshallable with
   | `Shallow ->
     (* TASSI: we should do something more sensible here *)
-    let _, initial_prefix =
-      CList.split_when (function _, CompilingLibrary _ -> true | _ -> false)
+    let lib_stk =
+      CList.map_filter (function
+        | _, Leaf _ -> None
+        | n, (CompilingLibrary _ as x) -> Some (n,x)
+        | n, OpenedModule (it,e,op,_) ->
+               Some(n,OpenedModule(it,e,op,Summary.empty_frozen))
+        | n, ClosedModule _ -> Some (n,ClosedModule [])
+        | n, OpenedSection (op, _) ->
+               Some(n,OpenedSection(op,Summary.empty_frozen))
+        | n, ClosedSection _ -> Some (n,ClosedSection [])
+        | _, FrozenState _ -> None)
       !lib_stk in
-    !comp_name, initial_prefix
+    !comp_name, lib_stk
   | _ ->
     !comp_name, !lib_stk
 
diff --git a/library/summary.mli b/library/summary.mli
index f6a9c6951..1ce09e12c 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -57,6 +57,7 @@ val nop : unit -> unit
 
 type frozen
 
+val empty_frozen : frozen
 val freeze_summaries : marshallable:marshallable -> frozen
 val unfreeze_summaries : frozen -> unit
 val init_summaries : unit -> unit
-- 
cgit v1.2.3