diff options
Diffstat (limited to 'library/states.mli')
| -rw-r--r-- | library/states.mli | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/library/states.mli b/library/states.mli index d186bf1c8..da6f33d65 100644 --- a/library/states.mli +++ b/library/states.mli @@ -22,18 +22,6 @@ val unfreeze : state -> unit (** {6 Rollback } *) -(** [with_heavy_rollback f h x] applies [f] to [x]. If this application - ends on an exception, the wrapper [h] is applied to it, then - the state of the whole system is restored as it was before applying [f], - and finally the exception produced by [h] is raised. *) - -val with_heavy_rollback : ('a -> 'b) -> (exn -> exn) -> 'a -> 'b - -(** [without_rollback] is just like [with_heavy_rollback], except that - no state is restored in case of exception. *) - -val without_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 applying [f] *) |