diff options
Diffstat (limited to 'ide/ide_slave.ml')
| -rw-r--r-- | ide/ide_slave.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 08f49ae5d..4171eb20d 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -100,7 +100,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 (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 @@ -301,7 +301,7 @@ let dirpath_of_string_list s = let id = try Nametab.full_name_module qid with Not_found -> - CErrors.errorlabstrm "Search.interface_search" + CErrors.user_err ~hdr:"Search.interface_search" (str "Module " ++ str path ++ str " not found.") in id |