From 60b1e4b4cc6783013e055838f5f2f5cca10f7d75 Mon Sep 17 00:00:00 2001
From: filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 29 Sep 1999 07:34:20 +0000
Subject: with_heavy_rollback deplace dans States

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@89 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/states.ml | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'library/states.ml')

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
-- 
cgit v1.2.3