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 4fbc4c886..c4e766095 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -31,14 +31,14 @@ let (extern_state,intern_state) =
let with_heavy_rollback f x =
let st = freeze () in
- try
+ try
f x
with reraise ->
(unfreeze st; raise reraise)
let with_state_protection f x =
let st = freeze () in
- try
+ try
let a = f x in unfreeze st; a
with reraise ->
(unfreeze st; raise reraise)