From fc579fdc83b751a44a18d2373e86ab38806e7306 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 19 Aug 2016 02:35:47 +0200 Subject: Make the user_err header an optional parameter. Suggested by @ppedrot --- checker/safe_typing.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'checker/safe_typing.ml') diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index c0b3a3e73..f7cd4d6f6 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -89,6 +89,6 @@ let import file clib univs digest = let unsafe_import file clib univs digest = let env = !genv in if !Flags.debug then check_imports Feedback.msg_warning clib.comp_name env clib.comp_deps - else check_imports (user_err"unsafe_import") clib.comp_name env clib.comp_deps; + else check_imports (user_err (str "unsafe_import")) clib.comp_name env clib.comp_deps; check_engagement env clib.comp_enga; full_add_module clib.comp_name clib.comp_mod univs digest -- cgit v1.2.3