aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/states.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-12-12 16:40:32 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-12-17 15:05:04 +0100
commit433f0bc4e5110db09c770022b277c419f8b35f64 (patch)
tree12f881fa7bbc72783dc2be9e7df7c39b05a7bbc7 /library/states.ml
parent5f2f22e7ff5d53e3258affa0e0e41666d5e0691d (diff)
Summary: more surgery functions
API to let one forge a frozen state out of another frozen state plus some frozen bits
Diffstat (limited to 'library/states.ml')
-rw-r--r--library/states.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/library/states.ml b/library/states.ml
index 200b14517..de03ca7c0 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -11,6 +11,8 @@ open System
type state = Lib.frozen * Summary.frozen
+let summary_of_state = snd
+
let freeze ~marshallable =
(Lib.freeze ~marshallable, Summary.freeze_summaries ~marshallable)