From 86116b181bb866c7f63a37796e1388f731ce7204 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 26 Jan 2017 11:38:19 +0100 Subject: [native comp] Improve error message on linking error. The native compiler doesn't support `Require` inside `Module` sections in some cases, we improve the error message. See: https://coq.inria.fr/bugs/show_bug.cgi?id=4335 This patch improves the error message and gives the user some feedback. --- kernel/safe_typing.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'kernel/safe_typing.ml') diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 8b28cd87b..7e28b1c56 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -795,7 +795,10 @@ type compiled_library = { type native_library = Nativecode.global list let get_library_native_symbols senv dir = - DPMap.find dir senv.native_symbols + try DPMap.find dir senv.native_symbols + with Not_found -> Errors.errorlabstrm "get_library_native_symbols" + Pp.((str "Linker error in the native compiler. Are you using Require inside a nested Module declaration?") ++ fnl () ++ + (str "This use case is not supported, but disabling the native compiler may help.")) (** FIXME: MS: remove?*) let current_modpath senv = senv.modpath -- cgit v1.2.3