diff options
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index e3b87bbe1..caaaff1b8 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -62,6 +62,8 @@ open Names open Declarations open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration + (** {6 Safe environments } Fields of [safe_environment] : @@ -69,7 +71,7 @@ open Context.Named.Declaration - [env] : the underlying environment (cf Environ) - [modpath] : the current module name - [modvariant] : - * NONE before coqtop initialization (or when -notop is used) + * NONE before coqtop initialization * LIBRARY at toplevel of a compilation or a regular coqtop session * STRUCT (params,oldsenv) : inside a local module, with module parameters [params] and earlier environment [oldsenv] @@ -361,7 +363,7 @@ let check_required current_libs needed = cost too much. *) let safe_push_named d env = - let id = get_id d in + let id = NamedDecl.get_id d in let _ = try let _ = Environ.lookup_named id env in @@ -795,7 +797,7 @@ type native_library = Nativecode.global list let get_library_native_symbols senv dir = try DPMap.find dir senv.native_symbols - with Not_found -> CErrors.errorlabstrm "get_library_native_symbols" + with Not_found -> CErrors.user_err ~hdr:"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.")) @@ -819,7 +821,7 @@ let export ?except senv dir = try join_safe_environment ?except senv with e -> let e = CErrors.push e in - CErrors.errorlabstrm "export" (CErrors.iprint e) + CErrors.user_err ~hdr:"export" (CErrors.iprint e) in assert(senv.future_cst = []); let () = check_current_library dir senv in @@ -855,7 +857,7 @@ let import lib cst vodigest senv = check_required senv.required lib.comp_deps; check_engagement senv.env lib.comp_enga; if DirPath.equal (ModPath.dp senv.modpath) lib.comp_name then - CErrors.errorlabstrm "Safe_typing.import" + CErrors.user_err ~hdr:"Safe_typing.import" (Pp.strbrk "Cannot load a library with the same name as the current one."); let mp = MPfile lib.comp_name in let mb = lib.comp_mod in |