1 files changed, 13 insertions, 0 deletions
diff --git a/library/states.ml b/library/states.ml
index 2e198e36f..d8fed1437 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -20,3 +20,16 @@ let (extern_state,intern_state) =
   let (raw_extern, raw_intern) = extern_intern state_magic_number ".coq" in
   (fun s -> raw_extern s (get_state())),
   (fun s -> set_state (raw_intern s))
+
+(* Rollback. *)
+
+let with_heavy_rollback f x =
+  let sum = freeze_summaries ()
+  and flib = freeze() in
+  try 
+    f x
+  with reraise -> begin
+    unfreeze_summaries sum;
+    unfreeze flib;
+    raise reraise
+  end