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/summary.mli | |
| parent | f8970ec2140662274bb10f0eb8d3ca72924835c7 (diff) | |
STM: modules do not prevent proofs from being ASync
Diffstat (limited to 'library/summary.mli')
| -rw-r--r-- | library/summary.mli | 1 |
1 files changed, 1 insertions, 0 deletions
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 |