aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/states.ml6
1 files changed, 2 insertions, 4 deletions
diff --git a/library/states.ml b/library/states.ml
index 90303a2a5c..c656dfb952 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -8,8 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Util
-
type state = Lib.frozen * Summary.frozen
let lib_of_state = fst
@@ -31,5 +29,5 @@ let with_state_protection f x =
try
let a = f x in unfreeze st; a
with reraise ->
- let reraise = CErrors.push reraise in
- (unfreeze st; iraise reraise)
+ let reraise = Exninfo.capture reraise in
+ (unfreeze st; Exninfo.iraise reraise)