aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/states.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/states.ml')
-rw-r--r--library/states.ml11
1 files changed, 0 insertions, 11 deletions
diff --git a/library/states.ml b/library/states.ml
index 1fd3fa2e5..93b2c120e 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -32,17 +32,6 @@ let (extern_state,intern_state) =
(* Rollback. *)
-let with_heavy_rollback f h x =
- let st = freeze ~marshallable:false in
- try
- f x
- with reraise ->
- let e = h reraise in (unfreeze st; raise e)
-
-let without_rollback f h x =
- try f x
- with reraise -> raise (h reraise)
-
let with_state_protection f x =
let st = freeze ~marshallable:false in
try