aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/indfun_common.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/indfun_common.ml')
-rw-r--r--plugins/funind/indfun_common.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index f56e92414..a1c94f8cb 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -110,7 +110,7 @@ let const_of_id id =
in
try Constrintern.locate_reference princ_ref
with Not_found ->
- CErrors.errorlabstrm "IndFun.const_of_id"
+ CErrors.user_err "IndFun.const_of_id"
(str "cannot find " ++ Nameops.pr_id id)
let def_of_const t =