aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/explainErr.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index d328ad0cf..fc3495796 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -32,6 +32,7 @@ let explain_exn_default = function
| Sys_error msg -> hov 0 (str "System error: " ++ guill msg)
| Out_of_memory -> hov 0 (str "Out of memory.")
| Stack_overflow -> hov 0 (str "Stack overflow.")
+ | Dynlink.Error e -> hov 0 (str "Dynlink error: " ++ str Dynlink.(error_message e))
| Timeout -> hov 0 (str "Timeout!")
| Sys.Break -> hov 0 (fnl () ++ str "User interrupt.")
(* Exceptions with pre-evaluated error messages *)