diff options
Diffstat (limited to 'vernac/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 3cf4b4a89d..953faf6fdb 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -342,9 +342,9 @@ let dump_universes_gen prl g s = close (); str "Universes written to file \"" ++ str s ++ str "\"." with reraise -> - let reraise = CErrors.push reraise in + let reraise = Exninfo.capture reraise in close (); - iraise reraise + Exninfo.iraise reraise let universe_subgraph ?loc g univ = let open Univ in |