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 --- ide/ide_slave.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'ide') diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index db0f96715..1d215f4ca 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -96,7 +96,7 @@ let is_undo cmd = match cmd with (** Check whether a command is forbidden by CoqIDE *) let coqide_cmd_checks (loc,ast) = - let user_error s = CErrors.user_err ~loc "CoqIde" (str s) in + let user_error s = CErrors.user_err ~loc ~hdr:"CoqIde" (str s) in if is_debug ast then user_error "Debug mode not available within CoqIDE"; if is_known_option ast then @@ -300,7 +300,7 @@ let dirpath_of_string_list s = let id = try Nametab.full_name_module qid with Not_found -> - CErrors.user_err "Search.interface_search" + CErrors.user_err ~hdr:"Search.interface_search" (str "Module " ++ str path ++ str " not found.") in id -- cgit v1.2.3