aboutsummaryrefslogtreecommitdiff
path: root/vernac/declareDef.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/declareDef.ml')
-rw-r--r--vernac/declareDef.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index e57c324c9a..2b6f987fa6 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -37,9 +37,9 @@ module Hook = struct
let call ?hook ?fix_exn x =
try Option.iter (fun hook -> CEphemeron.get hook x) hook
with e when CErrors.noncritical e ->
- let e = CErrors.push e in
+ let e = Exninfo.capture e in
let e = Option.cata (fun fix -> fix e) e fix_exn in
- Util.iraise e
+ Exninfo.iraise e
end
(* Locality stuff *)