diff options
Diffstat (limited to 'vernac/declareDef.ml')
| -rw-r--r-- | vernac/declareDef.ml | 4 |
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 *) |
