diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-01-04 10:32:22 +0100 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-01-05 17:13:58 +0100 |
commit | 24ca86389b32e42199db8faadd41918e162b8d46 (patch) | |
tree | 099e8eae42dfc98eb8ac480f385b2ffec120471b /library/lib.ml | |
parent | f8970ec2140662274bb10f0eb8d3ca72924835c7 (diff) |
STM: modules do not prevent proofs from being ASync
Diffstat (limited to 'library/lib.ml')
-rw-r--r-- | library/lib.ml | 15 |
1 files changed, 12 insertions, 3 deletions
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 |