diff options
Diffstat (limited to 'library/states.ml')
| -rw-r--r-- | library/states.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/library/states.ml b/library/states.ml index eb597670f..8b8193981 100644 --- a/library/states.ml +++ b/library/states.ml @@ -39,6 +39,10 @@ let with_heavy_rollback f h 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 () in try |