with_heavy_rollback deplace dans States

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@89 85f007b7-540e-0410-9357-904b9bb8a0f7

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