aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/states.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/states.ml')
-rw-r--r--library/states.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/library/states.ml b/library/states.ml
index d8fed1437..be1241a9a 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -23,6 +23,9 @@ let (extern_state,intern_state) =
(* Rollback. *)
+let freeze = get_state
+let unfreeze = set_state
+
let with_heavy_rollback f x =
let sum = freeze_summaries ()
and flib = freeze() in