diff options
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index e9be955e8..c89766fb9 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -688,7 +688,9 @@ let export compilation_mode senv dir = try if compilation_mode = Flags.BuildVi then { senv with future_cst = [] } else join_safe_environment senv - with e -> Errors.errorlabstrm "export" (Errors.print e) + with e -> + let e = Errors.push e in + Errors.errorlabstrm "export" (Errors.print e) in assert(senv.future_cst = []); let () = check_current_library dir senv in |