aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/states.mli
diff options
context:
space:
mode:
Diffstat (limited to 'library/states.mli')
-rw-r--r--library/states.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/library/states.mli b/library/states.mli
index 70d139d36..4f114d576 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -25,7 +25,7 @@ val unfreeze : state -> unit
(** [with_heavy_rollback f x] applies [f] to [x] and restores the
state of the whole system as it was before the evaluation if an exception
is raised. *)
-val with_heavy_rollback : ('a -> 'b) -> 'a -> 'b
+val with_heavy_rollback : ('a -> 'b) -> (exn -> exn) -> 'a -> 'b
(** [with_state_protection f x] applies [f] to [x] and restores the
state of the whole system as it was before the evaluation of f *)