aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2016-08-19 02:35:47 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2016-08-19 02:46:38 +0200
commitfc579fdc83b751a44a18d2373e86ab38806e7306 (patch)
treeb325c2ff65c505ad62ac7b3fce6bce28633a60f0 /ide
parent543ee0c7ad43874c577416af9f2e5a94d7d1e4d3 (diff)
Make the user_err header an optional parameter.
Suggested by @ppedrot
Diffstat (limited to 'ide')
-rw-r--r--ide/ide_slave.ml4
1 files changed, 2 insertions, 2 deletions
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