aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/states.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/states.ml')
-rw-r--r--library/states.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/library/states.ml b/library/states.ml
index b7c66abf5..4619b3b53 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -28,12 +28,12 @@ let (extern_state,intern_state) =
(* Rollback. *)
-let with_heavy_rollback f x =
+let with_heavy_rollback f h x =
let st = freeze () in
try
f x
with reraise ->
- (unfreeze st; raise reraise)
+ let e = h reraise in (unfreeze st; raise e)
let with_state_protection f x =
let st = freeze () in